let K be Field; :: thesis: for V1 being VectSp of K
for f being linear-transformation of V1,V1 holds f | (UnionKers f) is linear-transformation of (UnionKers f),(UnionKers f)
let V1 be VectSp of K; :: thesis: for f being linear-transformation of V1,V1 holds f | (UnionKers f) is linear-transformation of (UnionKers f),(UnionKers f)
let f be linear-transformation of V1,V1; :: thesis: f | (UnionKers f) is linear-transformation of (UnionKers f),(UnionKers f)
set U = UnionKers f;
rng (f | (UnionKers f)) c= the carrier of (UnionKers f)

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (f | (UnionKers f)) or y in the carrier of (UnionKers f) )
assume y in rng (f | (UnionKers f)) ; :: thesis: y in the carrier of (UnionKers f)
then consider x being object such that
A1: x in dom (f | (UnionKers f)) and
A2: (f | (UnionKers f)) . x = y by FUNCT_1:def 3;
x in the carrier of (UnionKers f) by A1, FUNCT_2:def 1;
then A3: x in UnionKers f ;
then x in V1 by VECTSP_4:9;
then reconsider v = x as Vector of V1 ;
consider n being Nat such that
A4: (f |^ n) . v = 0. V1 by A3, Th24;
A5: dom f = [#] V1 by FUNCT_2:def 1;
0. V1 = (f |^ (n + 1)) . v by A4, Th23
.= ((f |^ n) * (f |^ 1)) . v by Th20
.= ((f |^ n) * f) . v by Th19
.= (f |^ n) . (f . v) by A5, FUNCT_1:13 ;
then A6: f . v in UnionKers f by Th24;
y = f . v by A1, A2, FUNCT_1:47;
hence y in the carrier of (UnionKers f) by A6; :: thesis: verum

end;

hence f | (UnionKers f) is linear-transformation of (UnionKers f),(UnionKers f) by Lm1, FUNCT_2:6; :: thesis: verum