defpred S₁[ Nat, Element of F₁()] means ( ( $1 < F₂() & $2 = F₃($1) ) or ( $1 >= F₂() & $2 = 0. F₁() ) );
A1: for x being Element of NAT ex y being Element of F₁() st S₁[x,y]

proof

let x be Element of NAT ; :: thesis: ex y being Element of F₁() st S₁[x,y]
( x < F₂() implies ( x < F₂() & F₃(x) = F₃(x) ) ) ;
hence ex y being Element of F₁() st S₁[x,y] ; :: thesis: verum

end;

ex f being sequence of the carrier of F₁() st
for x being Element of NAT holds S₁[x,f . x] from FUNCT_2:sch 3(A1);
then consider f being sequence of the carrier of F₁() such that
A2: for x being Element of NAT holds
( ( x < F₂() & f . x = F₃(x) ) or ( x >= F₂() & f . x = 0. F₁() ) ) ;
ex n being Nat st
for i being Nat st i >= n holds
f . i = 0. F₁()

proof

reconsider n = F₂() as Element of NAT by ORDINAL1:def 12;
take n ; :: thesis: for i being Nat st i >= n holds
f . i = 0. F₁()
let i be Nat; :: thesis: ( i >= n implies f . i = 0. F₁() )
i in NAT by ORDINAL1:def 12;
hence ( i >= n implies f . i = 0. F₁() ) by A2; :: thesis: verum

end;

then reconsider f = f as AlgSequence of F₁() by Def1;
take f ; :: thesis: ( len f <= F₂() & ( for k being Nat st k < F₂() holds
f . k = F₃(k) ) )

now :: thesis: for i being Nat st i >= F₂() holds
f . i = 0. F₁()

let i be Nat; :: thesis: ( i >= F₂() implies f . i = 0. F₁() )
assume A3: i >= F₂() ; :: thesis: f . i = 0. F₁()
i in NAT by ORDINAL1:def 12;
hence f . i = 0. F₁() by A2, A3; :: thesis: verum

end;

then F₂() is_at_least_length_of f ;
hence len f <= F₂() by Def3; :: thesis: for k being Nat st k < F₂() holds
f . k = F₃(k)
let k be Nat; :: thesis: ( k < F₂() implies f . k = F₃(k) )
k in NAT by ORDINAL1:def 12;
hence ( k < F₂() implies f . k = F₃(k) ) by A2; :: thesis: verum