Corollary

Tag 05TA, permanent. Cite it as [Bourbaki, Tag 05TA].

For every $K$ -linear mapping $f : E' \to E$ , $\operatorname{Im}(f_{(A)}) = (\operatorname{Im}(f))_{(A)}$ , $\operatorname{Ker}(f_{(A)}) = (\operatorname{Ker}(f))_{(A)}$ , $\operatorname{Coker}(f_{(A)}) = (\operatorname{Coker}(f))_{(A)}$ , to within canonical isomorphisms.

Bourbaki puts the proof directly after the statement, so what is above is the statement and its proof together.