defpred S1[ Element of NAT , Element of F1()] means ( ( \$1 < F2() & \$2 = F3(\$1) ) or ( \$1 >= F2() & \$2 = 0. F1() ) );
A1: for x being Element of NAT ex y being Element of F1() st S1[x,y]
proof
let x be Element of NAT ; :: thesis: ex y being Element of F1() st S1[x,y]
( x < F2() implies ( x < F2() & F3(x) = F3(x) ) ) ;
hence ex y being Element of F1() st S1[x,y] ; :: thesis: verum
end;
ex f being sequence of the carrier of F1() st
for x being Element of NAT holds S1[x,f . x] from then consider f being sequence of the carrier of F1() such that
A2: for x being Element of NAT holds
( ( x < F2() & f . x = F3(x) ) or ( x >= F2() & f . x = 0. F1() ) ) ;
ex n being Nat st
for i being Nat st i >= n holds
f . i = 0. F1()
proof
take F2() ; :: thesis: for i being Nat st i >= F2() holds
f . i = 0. F1()

let i be Nat; :: thesis: ( i >= F2() implies f . i = 0. F1() )
i in NAT by ORDINAL1:def 12;
hence ( i >= F2() implies f . i = 0. F1() ) by A2; :: thesis: verum
end;
then reconsider f = f as AlgSequence of F1() by ALGSEQ_1:def 1;
take f ; :: thesis: ( len f <= F2() & ( for n being Element of NAT st n < F2() holds
f . n = F3(n) ) )

now :: thesis: for i being Nat st i >= F2() holds
f . i = 0. F1()
let i be Nat; :: thesis: ( i >= F2() implies f . i = 0. F1() )
i in NAT by ORDINAL1:def 12;
hence ( i >= F2() implies f . i = 0. F1() ) by A2; :: thesis: verum
end;
then F2() is_at_least_length_of f ;
hence ( len f <= F2() & ( for n being Element of NAT st n < F2() holds
f . n = F3(n) ) ) by ; :: thesis: verum