let n be Nat; :: thesis: for K being Field
for V1 being VectSp of K
for f being linear-transformation of V1,V1 st UnionKers f = ker (f |^ n) holds
(ker (f |^ n)) /\ (im (f |^ n)) = (0). V1
let K be Field; :: thesis: for V1 being VectSp of K
for f being linear-transformation of V1,V1 st UnionKers f = ker (f |^ n) holds
(ker (f |^ n)) /\ (im (f |^ n)) = (0). V1
let V1 be VectSp of K; :: thesis: for f being linear-transformation of V1,V1 st UnionKers f = ker (f |^ n) holds
(ker (f |^ n)) /\ (im (f |^ n)) = (0). V1
let f be linear-transformation of V1,V1; :: thesis: ( UnionKers f = ker (f |^ n) implies (ker (f |^ n)) /\ (im (f |^ n)) = (0). V1 )
set KER = ker (f |^ n);
set IM = im (f |^ n);
assume A1: UnionKers f = ker (f |^ n) ; :: thesis: (ker (f |^ n)) /\ (im (f |^ n)) = (0). V1
the carrier of ((ker (f |^ n)) /\ (im (f |^ n))) c= {(0. V1)}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of ((ker (f |^ n)) /\ (im (f |^ n))) or x in {(0. V1)} )
assume x in the carrier of ((ker (f |^ n)) /\ (im (f |^ n))) ; :: thesis: x in {(0. V1)}
then A2: x in (ker (f |^ n)) /\ (im (f |^ n)) ;
then x in V1 by VECTSP_4:9;
then reconsider v = x as Vector of V1 ;
v in im (f |^ n) by A2, VECTSP_5:3;
then consider w being Element of V1 such that
A3: (f |^ n) . w = v by RANKNULL:13;
A4: dom (f |^ n) = the carrier of V1 by FUNCT_2:def 1;
v in ker (f |^ n) by A2, VECTSP_5:3;
then 0. V1 = (f |^ n) . ((f |^ n) . w) by A3, RANKNULL:10
.= ((f |^ n) * (f |^ n)) . w by A4, FUNCT_1:13
.= (f |^ (n + n)) . w by Th20 ;
then w in ker (f |^ n) by A1, Th24;
then v = 0. V1 by A3, RANKNULL:10;
hence x in {(0. V1)} by TARSKI:def 1; :: thesis: verum

end;

then the carrier of ((ker (f |^ n)) /\ (im (f |^ n))) = {(0. V1)} by ZFMISC_1:33
.= the carrier of ((0). V1) by VECTSP_4:def 3 ;
hence (ker (f |^ n)) /\ (im (f |^ n)) = (0). V1 by VECTSP_4:29; :: thesis: verum