defpred S₁[ set , set ] means ex k being Element of NAT st
( k = $1 & ( ( k < len M & $2 = M * (k + 1),1 ) or ( len M <= k & $2 = 0. L ) ) );
A1: for x being set st x in NAT holds
ex y being set st
( y in the carrier of L & S₁[x,y] )

proof

let u be set ; :: thesis: ( u in NAT implies ex y being set st
( y in the carrier of L & S₁[u,y] ) )
assume u in NAT ; :: thesis: ex y being set st
( y in the carrier of L & S₁[u,y] )
then reconsider u9 = u as Element of NAT ;
thus ex y being set st
( y in the carrier of L & S₁[u,y] ) :: thesis: verum

proof

per cases ( u9 < len M or u9 >= len M ) ;

suppose A2: u9 < len M ; :: thesis: ex y being set st
( y in the carrier of L & S₁[u,y] )

take y = M * (u9 + 1),1; :: thesis: ( y in the carrier of L & S₁[u,y] )
thus ( y in the carrier of L & S₁[u,y] ) by A2; :: thesis: verum

end;

suppose A3: u9 >= len M ; :: thesis: ex y being set st
( y in the carrier of L & S₁[u,y] )

take y = 0. L; :: thesis: ( y in the carrier of L & S₁[u,y] )
thus ( y in the carrier of L & S₁[u,y] ) by A3; :: thesis: verum

end;

end;

end;

end;

consider f being Function of NAT ,the carrier of L such that
A4: for x being set st x in NAT holds
S₁[x,f . x] from FUNCT_2:sch 1(A1);
reconsider f = f as sequence of L ;
ex n being Nat st
for i being Nat st i >= n holds
f . i = 0. L

proof

take len M ; :: thesis: for i being Nat st i >= len M holds
f . i = 0. L

now

let i be Nat; :: thesis: ( i >= len M implies f . i = 0. L )
i in NAT by ORDINAL1:def 13;
then A5: ex k being Element of NAT st
( k = i & ( ( k < len M & f . i = M * (k + 1),1 ) or ( len M <= k & f . i = 0. L ) ) ) by A4;
assume i >= len M ; :: thesis: f . i = 0. L
hence f . i = 0. L by A5; :: thesis: verum

end;

hence for i being Nat st i >= len M holds
f . i = 0. L ; :: thesis: verum

end;

then reconsider q = f as AlgSequence of L by ALGSEQ_1:def 2;

A6: now

let i be Nat; :: thesis: ( i >= len M implies q . i = 0. L )
i in NAT by ORDINAL1:def 13;
then A7: ex k being Element of NAT st
( k = i & ( ( k < len M & q . i = M * (k + 1),1 ) or ( len M <= k & q . i = 0. L ) ) ) by A4;
assume i >= len M ; :: thesis: q . i = 0. L
hence q . i = 0. L by A7; :: thesis: verum

end;

take q ; :: thesis: ( ( for i being Nat st i < len M holds
q . i = M * (i + 1),1 ) & ( for i being Nat st i >= len M holds
q . i = 0. L ) )

now

let i be Nat; :: thesis: ( i < len M implies q . i = M * (i + 1),1 )
i in NAT by ORDINAL1:def 13;
then A8: ex k being Element of NAT st
( k = i & ( ( k < len M & q . i = M * (k + 1),1 ) or ( len M <= k & q . i = 0. L ) ) ) by A4;
assume i < len M ; :: thesis: q . i = M * (i + 1),1
hence q . i = M * (i + 1),1 by A8; :: thesis: verum

end;

hence ( ( for i being Nat st i < len M holds
q . i = M * (i + 1),1 ) & ( for i being Nat st i >= len M holds
q . i = 0. L ) ) by A6; :: thesis: verum