defpred S_{1}[ Nat, Element of F_{1}()] means ( ( $1 < F_{2}() & $2 = F_{3}($1) ) or ( $1 >= F_{2}() & $2 = 0. F_{1}() ) );

A1: for x being Element of NAT ex y being Element of F_{1}() st S_{1}[x,y]
_{1}() st

for x being Element of NAT holds S_{1}[x,f . x]
from FUNCT_2:sch 3(A1);

then consider f being sequence of the carrier of F_{1}() such that

A2: for x being Element of NAT holds

( ( x < F_{2}() & f . x = F_{3}(x) ) or ( x >= F_{2}() & f . x = 0. F_{1}() ) )
;

ex n being Nat st

for i being Nat st i >= n holds

f . i = 0. F_{1}()
_{1}() by Def1;

take f ; :: thesis: ( len f <= F_{2}() & ( for k being Nat st k < F_{2}() holds

f . k = F_{3}(k) ) )

_{2}() is_at_least_length_of f
;

hence len f <= F_{2}()
by Def3; :: thesis: for k being Nat st k < F_{2}() holds

f . k = F_{3}(k)

let k be Nat; :: thesis: ( k < F_{2}() implies f . k = F_{3}(k) )

k in NAT by ORDINAL1:def 12;

hence ( k < F_{2}() implies f . k = F_{3}(k) )
by A2; :: thesis: verum

A1: for x being Element of NAT ex y being Element of F

proof

ex f being sequence of the carrier of F
let x be Element of NAT ; :: thesis: ex y being Element of F_{1}() st S_{1}[x,y]

( x < F_{2}() implies ( x < F_{2}() & F_{3}(x) = F_{3}(x) ) )
;

hence ex y being Element of F_{1}() st S_{1}[x,y]
; :: thesis: verum

end;( x < F

hence ex y being Element of F

for x being Element of NAT holds S

then consider f being sequence of the carrier of F

A2: for x being Element of NAT holds

( ( x < F

ex n being Nat st

for i being Nat st i >= n holds

f . i = 0. F

proof

then reconsider f = f as AlgSequence of F
reconsider n = F_{2}() as Element of NAT by ORDINAL1:def 12;

take n ; :: thesis: for i being Nat st i >= n holds

f . i = 0. F_{1}()

let i be Nat; :: thesis: ( i >= n implies f . i = 0. F_{1}() )

i in NAT by ORDINAL1:def 12;

hence ( i >= n implies f . i = 0. F_{1}() )
by A2; :: thesis: verum

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

take f ; :: thesis: ( len f <= F

f . k = F

now :: thesis: for i being Nat st i >= F_{2}() holds

f . i = 0. F_{1}()

then
Ff . i = 0. F

let i be Nat; :: thesis: ( i >= F_{2}() implies f . i = 0. F_{1}() )

assume A3: i >= F_{2}()
; :: thesis: f . i = 0. F_{1}()

i in NAT by ORDINAL1:def 12;

hence f . i = 0. F_{1}()
by A2, A3; :: thesis: verum

end;assume A3: i >= F

i in NAT by ORDINAL1:def 12;

hence f . i = 0. F

hence len f <= F

f . k = F

let k be Nat; :: thesis: ( k < F

k in NAT by ORDINAL1:def 12;

hence ( k < F