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 object ; :: 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 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
then ex v being Vector of V1 st
( x = v & ex n being Nat st (f |^ n) . v = 0. V1 ) ;
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 ;
then A1: 0. V1 in S ;

A2: now :: thesis: for v, u being Element of V1 st v in S & u in S holds
v + u in S

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

now :: thesis: v + u in S

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 VECTSP_1:def 20
.= (0. V1) + (0. V1) by A5, A6, Th23
.= 0. V1 by RLVECT_1:def 4 ;
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 VECTSP_1:def 20
.= (0. V1) + (0. V1) by A5, A6, Th23
.= 0. V1 by RLVECT_1:def 4 ;
hence v + u in S ; :: thesis: verum

end;

end;

end;

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

end;

now :: thesis: for a being Element of K
for v being Element of V1 st v in S holds
a * v in S

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 v in S ; :: thesis: a * v in S
then ex v9 being Vector of V1 st
( v9 = v & ex n being Nat st (f |^ n) . v9 = 0. V1 ) ;
then consider n being Nat such that
A7: (f |^ n) . v = 0. V1 ;
(f |^ n) . (a * v) = a * (0. V1) by A7, MOD_2:def 2
.= 0. V1 by VECTSP_1:14 ;
hence a * v in S ; :: thesis: verum

end;

then S is linearly-closed by A2;
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 A1, VECTSP_4:34; :: thesis: verum