defpred S1[ 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
reconsider n = F2() as Element of NAT by ORDINAL1:def 12;
take n ; :: thesis: for i being Nat st i >= n holds
f . i = 0. F1()

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

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() )
assume A3: i >= F2() ; :: thesis: f . i = 0. F1()
i in NAT by ORDINAL1:def 12;
hence f . i = 0. F1() by A2, A3; :: thesis: verum
end;
then F2() is_at_least_length_of f ;
hence len f <= F2() by Def3; :: thesis: for k being Nat st k < F2() holds
f . k = F3(k)

let k be Nat; :: thesis: ( k < F2() implies f . k = F3(k) )
k in NAT by ORDINAL1:def 12;
hence ( k < F2() implies f . k = F3(k) ) by A2; :: thesis: verum