defpred S_{1}[ 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_{1}[x,y] )

A4: for x being object st x in NAT holds

S_{1}[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

q . i = M * ((i + 1),1) ) & ( for i being Nat st i >= len M holds

q . i = 0. L ) )

q . i = M * ((i + 1),1) ) & ( for i being Nat st i >= len M holds

q . i = 0. L ) ) by A6; :: thesis: verum

( 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

proof

consider f being sequence of the carrier of L such that
let u be object ; :: thesis: ( u in NAT implies ex y being object st

( y in the carrier of L & S_{1}[u,y] ) )

assume u in NAT ; :: thesis: ex y being object st

( y in the carrier of L & S_{1}[u,y] )

then reconsider u9 = u as Element of NAT ;

thus ex y being object st

( y in the carrier of L & S_{1}[u,y] )
:: thesis: verum

end;( y in the carrier of L & S

assume u in NAT ; :: thesis: ex y being object st

( y in the carrier of L & S

then reconsider u9 = u as Element of NAT ;

thus ex y being object st

( y in the carrier of L & S

proof
end;

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

end;

A4: for x being object st x in NAT holds

S

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

then reconsider q = f as AlgSequence of L by ALGSEQ_1:def 1;
take
len M
; :: thesis: for i being Nat st i >= len M holds

f . i = 0. L

f . i = 0. L ; :: thesis: verum

end;f . i = 0. L

now :: thesis: for i being Nat st i >= len M holds

f . i = 0. L

hence
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;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

f . i = 0. L ; :: thesis: verum

A6: now :: thesis: for i being Nat st i >= len M holds

q . i = 0. L

take
q
; :: 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;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

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)

hence
( ( 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;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

q . i = M * ((i + 1),1) ) & ( for i being Nat st i >= len M holds

q . i = 0. L ) ) by A6; :: thesis: verum