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 linear-transformation of V2,V3 st g | (im f) is one-to-one holds
( rank (g * f) = rank f & nullity (g * f) = nullity f )
let V1, V2, V3 be finite-dimensional VectSp of K; :: thesis: for f being linear-transformation of V1,V2
for g being linear-transformation of V2,V3 st g | (im f) is one-to-one holds
( rank (g * f) = rank f & nullity (g * f) = nullity f )
let f be linear-transformation of V1,V2; :: thesis: for g being linear-transformation of V2,V3 st g | (im f) is one-to-one holds
( rank (g * f) = rank f & nullity (g * f) = nullity f )
let g be linear-transformation of V2,V3; :: thesis: ( g | (im f) is one-to-one implies ( rank (g * f) = rank f & nullity (g * f) = nullity f ) )
assume A1: g | (im f) is one-to-one ; :: thesis: ( rank (g * f) = rank f & nullity (g * f) = nullity f )
the carrier of (im (g * f)) = [#] (im (g * f))
.= (g * f) .: ([#] V1) by RANKNULL:def 2
.= ((g | (im f)) * f) .: ([#] V1) by Lm8
.= (g | (im f)) .: (f .: ([#] V1)) by RELAT_1:126
.= (g | (im f)) .: ([#] (im f)) by RANKNULL:def 2
.= [#] (im (g | (im f))) by RANKNULL:def 2
.= the carrier of (im (g | (im f))) ;
then A2: rank (g * f) = rank (g | (im f)) by VECTSP_4:29
.= rank f by A1, RANKNULL:45 ;
(nullity f) + (rank f) = dim V1 by RANKNULL:44
.= (nullity (g * f)) + (rank (g * f)) by RANKNULL:44 ;
hence ( rank (g * f) = rank f & nullity (g * f) = nullity f ) by A2; :: thesis: verum