let K be Field; :: thesis: for V1 being VectSp of K
for f being linear-transformation of V1,V1
for v1 being Vector of V1 holds
( v1 in UnionKers f iff ex n being Nat st (f |^ n) . v1 = 0. V1 )
let V1 be VectSp of K; :: thesis: for f being linear-transformation of V1,V1
for v1 being Vector of V1 holds
( v1 in UnionKers f iff ex n being Nat st (f |^ n) . v1 = 0. V1 )
let f be linear-transformation of V1,V1; :: thesis: for v1 being Vector of V1 holds
( v1 in UnionKers f iff ex n being Nat st (f |^ n) . v1 = 0. V1 )
let v1 be Vector of V1; :: thesis: ( v1 in UnionKers f iff ex n being Nat st (f |^ n) . v1 = 0. V1 )

hereby :: thesis: ( ex n being Nat st (f |^ n) . v1 = 0. V1 implies v1 in UnionKers f )

assume v1 in UnionKers f ; :: thesis: ex n being Nat st (f |^ n) . v1 = 0. V1
then v1 in the carrier of (UnionKers f) ;
then v1 in { w where w is Vector of V1 : ex n being Nat st (f |^ n) . w = 0. V1 } by Def5;
then ex w being Vector of V1 st
( v1 = w & ex m being Nat st (f |^ m) . w = 0. V1 ) ;
hence ex n being Nat st (f |^ n) . v1 = 0. V1 ; :: thesis: verum

end;

assume ex n being Nat st (f |^ n) . v1 = 0. V1 ; :: thesis: v1 in UnionKers f
then v1 in { w where w is Vector of V1 : ex n being Nat st (f |^ n) . w = 0. V1 } ;
then v1 in the carrier of (UnionKers f) by Def5;
hence v1 in UnionKers f ; :: thesis: verum