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;
A1: the carrier of (ker (f | I)) c= {(0. I)}

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of (ker (f | I)) or x in {(0. I)} )
assume A2: x in the carrier of (ker (f | I)) ; :: thesis: x in {(0. I)}
A3: x in ker (f | I) by A2, STRUCT_0:def 5;
then A4: x in I by VECTSP_4:17;
then reconsider v = x as Vector of I by STRUCT_0:def 5;
reconsider w = v as Vector of V1 by VECTSP_4:18;
A5: (UnionKers f) /\ I = (0). V1 by VECTSP_5:50;
0. I = 0. V1 by VECTSP_4:19
.= (f | I) . v by A3, RANKNULL:10
.= f . v by FUNCT_1:72 ;
then (f |^ 1) . w = 0. I by Th19
.= 0. V1 by VECTSP_4:19 ;
then v in UnionKers f by Th24;
then v in (UnionKers f) /\ I by A4, VECTSP_5:7;
then v in the carrier of ((0). V1) by A5, STRUCT_0:def 5;
then v in {(0. V1)} by VECTSP_4:def 3;
then v = 0. V1 by TARSKI:def 1
.= 0. I by VECTSP_4:19 ;
hence x in {(0. I)} by TARSKI:def 1; :: thesis: verum

end;

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