let K be Field; :: thesis: for V1 being VectSp of K
for f being linear-transformation of V1,V1
for I being Linear_Compl of UnionKers f holds f | I is one-to-one
let V1 be VectSp of K; :: thesis: for f being linear-transformation of V1,V1
for I being Linear_Compl of UnionKers f holds f | I is one-to-one
let f be linear-transformation of V1,V1; :: thesis: for I being Linear_Compl of UnionKers f holds f | I is one-to-one
let I be Linear_Compl of UnionKers f; :: thesis: f | I is one-to-one
set fI = f | I;
set U = UnionKers f;
the carrier of (ker (f | I)) c= {(0. I)}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of (ker (f | I)) or x in {(0. I)} )
assume x in the carrier of (ker (f | I)) ; :: thesis: x in {(0. I)}
then A1: x in ker (f | I) ;
then A2: x in I by VECTSP_4:9;
then reconsider v = x as Vector of I ;
reconsider w = v as Vector of V1 by VECTSP_4:10;
0. I = 0. V1 by VECTSP_4:11
.= (f | I) . v by A1, RANKNULL:10
.= f . v by FUNCT_1:49 ;
then (f |^ 1) . w = 0. I by Th19
.= 0. V1 by VECTSP_4:11 ;
then v in UnionKers f by Th24;
then ( (UnionKers f) /\ I = (0). V1 & v in (UnionKers f) /\ I ) by A2, VECTSP_5:3, VECTSP_5:40;
then v in the carrier of ((0). V1) ;
then v in {(0. V1)} by VECTSP_4:def 3;
then v = 0. V1 by TARSKI:def 1
.= 0. I by VECTSP_4:11 ;
hence x in {(0. I)} by TARSKI:def 1; :: thesis: verum

end;

then the carrier of (ker (f | I)) = {(0. I)} by ZFMISC_1:33
.= the carrier of ((0). I) by VECTSP_4:def 3 ;
then ker (f | I) = (0). I by VECTSP_4:29;
hence f | I is one-to-one by MATRLIN2:43; :: thesis: verum