set S = { v where v is Vector of : ex n being Nat st (f |^ n) . v = 0. V1 } ;
{ v where v is Vector of : 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 : 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 : ex n being Nat st (f |^ n) . v = 0. V1 } ; :: thesis: x in the carrier of V1
then ex v being Vector of 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 : ex n being Nat st (f |^ n) . v = 0. V1 } as Subset of ;
(f |^ 0 ) . (0. V1) = (id V1) . (0. V1) by Th18
.= 0. V1 by FUNCT_1:34 ;
then A1: 0. V1 in S ;

A2: now

let v, u be Element of ; :: 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 v' being Vector of st
( v' = v & ex n being Nat st (f |^ n) . v' = 0. V1 ) by A3;
then consider n being Nat such that
A5: (f |^ n) . v = 0. V1 ;
ex u' being Vector of st
( u' = u & ex m being Nat st (f |^ m) . u' = 0. V1 ) by A4;
then consider m being Nat such that
A6: (f |^ m) . u = 0. V1 ;

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 A5, A6, 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 A5, A6, 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 ; :: thesis: for v being Element of st v in S holds
a * v in S
let v be Element of ; :: thesis: ( v in S implies a * v in S )
assume v in S ; :: thesis: a * v in S
then ex v' being Vector of st
( v' = v & ex n being Nat st (f |^ n) . v' = 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 5
.= 0. V1 by VECTSP_1:59 ;
hence a * v in S ; :: thesis: verum

end;

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