defpred S_{1}[ Element of 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 ALGSEQ_1:def 1;

take f ; :: thesis: ( len f <= F_{2}() & ( for n being Element of NAT st n < F_{2}() holds

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

_{2}() is_at_least_length_of f
;

hence ( len f <= F_{2}() & ( for n being Element of NAT st n < F_{2}() holds

f . n = F_{3}(n) ) )
by A2, ALGSEQ_1:def 3; :: 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
take
F_{2}()
; :: thesis: for i being Nat st i >= F_{2}() holds

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

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

i in NAT by ORDINAL1:def 12;

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

end;f . i = 0. F

let i be Nat; :: thesis: ( i >= F

i in NAT by ORDINAL1:def 12;

hence ( i >= F

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

f . n = 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}() )

i in NAT by ORDINAL1:def 12;

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

end;i in NAT by ORDINAL1:def 12;

hence ( i >= F

hence ( len f <= F

f . n = F