let K be Field; :: thesis: for V1, V2, V3 being finite-dimensional VectSp of K
for f being linear-transformation of V1,V2
for g being Function of V2,V3 holds g * f = (g | (im f)) * f
let V1, V2, V3 be finite-dimensional VectSp of K; :: thesis: for f being linear-transformation of V1,V2
for g being Function of V2,V3 holds g * f = (g | (im f)) * f
let f be linear-transformation of V1,V2; :: thesis: for g being Function of V2,V3 holds g * f = (g | (im f)) * f
let g be Function of V2,V3; :: thesis: g * f = (g | (im f)) * f
dom f = [#] V1 by FUNCT_2:def 1;
then [#] (im f) = f .: (dom f) by RANKNULL:def 2
.= rng f by RELAT_1:113 ;
hence (g | (im f)) * f = (g * (id (rng f))) * f by RELAT_1:65
.= g * ((id (rng f)) * f) by RELAT_1:36
.= g * f by RELAT_1:54 ;
:: thesis: verum