defpred S₁[ object , object ] 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 object st x in NAT holds
ex y being object st
( y in the carrier of L & S₁[x,y] )

proof

let u be object ; :: thesis: ( u in NAT implies ex y being object st
( y in the carrier of L & S₁[u,y] ) )
assume u in NAT ; :: thesis: ex y being object st
( y in the carrier of L & S₁[u,y] )
then reconsider u9 = u as Element of NAT ;
thus ex y being object 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 object st
( y in the carrier of L & S₁[u,y] )

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

end;

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

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

end;

end;

end;

end;

consider f being sequence of the carrier of L such that
A4: for x being object 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 :: thesis: for i being Nat st i >= len M holds
f . i = 0. L

let i be Nat; :: thesis: ( i >= len M implies f . i = 0. L )
i in NAT by ORDINAL1:def 12;
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 1;

A6: now :: thesis: for i being Nat st i >= len M holds
q . i = 0. L

let i be Nat; :: thesis: ( i >= len M implies q . i = 0. L )
i in NAT by ORDINAL1:def 12;
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 :: thesis: for i being Nat st i < len M holds
q . i = M * ((i + 1),1)

let i be Nat; :: thesis: ( i < len M implies q . i = M * ((i + 1),1) )
i in NAT by ORDINAL1:def 12;
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