set S = { v where v is Vector of V1 : ex n being Nat st (f |^ n) . v = 0. V1 } ;
{ v where v is Vector of V1 : ex n being Nat st (f |^ n) . v = 0. V1 } c= the carrier of V1

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { v where v is Vector of V1 : ex n being Nat st (f |^ n) . v = 0. V1 } or x in the carrier of V1 )
assume A1: x in { v where v is Vector of V1 : ex n being Nat st (f |^ n) . v = 0. V1 } ; :: thesis: x in the carrier of V1
ex v being Vector of V1 st
( x = v & ex n being Nat st (f |^ n) . v = 0. V1 ) by A1;
hence x in the carrier of V1 ; :: thesis: verum

end;

then reconsider S = { v where v is Vector of V1 : ex n being Nat st (f |^ n) . v = 0. V1 } as Subset of V1 ;
(f |^ 0 ) . (0. V1) = (id V1) . (0. V1) by Th18
.= 0. V1 by FUNCT_1:34 ;
then A2: 0. V1 in S ;

A3: now

let v, u be Element of V1; :: thesis: ( v in S & u in S implies v + u in S )
assume A4: ( v in S & u in S ) ; :: thesis: v + u in S
consider v' being Vector of V1 such that
A5: ( v' = v & ex n being Nat st (f |^ n) . v' = 0. V1 ) by A4;
consider n being Nat such that
A6: (f |^ n) . v = 0. V1 by A5;
consider u' being Vector of V1 such that
A7: ( u' = u & ex m being Nat st (f |^ m) . u' = 0. V1 ) by A4;
consider m being Nat such that
A8: (f |^ m) . u = 0. V1 by A7;

now

per cases ( m <= n or m > n ) ;

suppose m <= n ; :: thesis: v + u in S

then reconsider i = n - m as Nat by NAT_1:21;
(f |^ n) . (v + u) = ((f |^ n) . v) + ((f |^ (m + i)) . u) by MOD_2:def 5
.= (0. V1) + (0. V1) by A6, A8, Th23
.= 0. V1 by RLVECT_1:def 7 ;
hence v + u in S ; :: thesis: verum

end;

suppose m > n ; :: thesis: v + u in S

then reconsider i = m - n as Nat by NAT_1:21;
(f |^ m) . (v + u) = ((f |^ m) . v) + ((f |^ (n + i)) . u) by MOD_2:def 5
.= (0. V1) + (0. V1) by A6, A8, Th23
.= 0. V1 by RLVECT_1:def 7 ;
hence v + u in S ; :: thesis: verum

end;

end;

end;

hence v + u in S ; :: thesis: verum

end;

now

let a be Element of K; :: thesis: for v being Element of V1 st v in S holds
a * v in S
let v be Element of V1; :: thesis: ( v in S implies a * v in S )
assume A9: v in S ; :: thesis: a * v in S
consider v' being Vector of V1 such that
A10: ( v' = v & ex n being Nat st (f |^ n) . v' = 0. V1 ) by A9;
consider n being Nat such that
A11: (f |^ n) . v = 0. V1 by A10;
(f |^ n) . (a * v) = a * (0. V1) by A11, MOD_2:def 5
.= 0. V1 by VECTSP_1:59 ;
hence a * v in S ; :: thesis: verum

end;

then S is linearly-closed by A3, VECTSP_4:def 1;
hence ex b₁ being strict Subspace of V1 st the carrier of b₁ = { v where v is Vector of V1 : ex n being Nat st (f |^ n) . v = 0. V1 } by A2, VECTSP_4:42; :: thesis: verum