reconsider S = Seg (F_{1}() + 1) as non empty set by FINSEQ_1:4;

consider z being FinSequence of F_{2}() such that

A1: len z = F_{1}() + 1
and

A2: for j being Nat st j in dom z holds

z . j = F_{3}(j)
from FINSEQ_2:sch 1();

take z ; :: thesis: ( len z = F_{1}() + 1 & ( for j being Nat of F_{1}() holds z . j = F_{3}(j) ) )

A3: dom z = Seg (F_{1}() + 1)
by A1, FINSEQ_1:def 3;

for j being Nat of F_{1}() holds z . j = F_{3}(j)
by Th7, A2, A3;

hence ( len z = F_{1}() + 1 & ( for j being Nat of F_{1}() holds z . j = F_{3}(j) ) )
by A1; :: thesis: verum

consider z being FinSequence of F

A1: len z = F

A2: for j being Nat st j in dom z holds

z . j = F

take z ; :: thesis: ( len z = F

A3: dom z = Seg (F

for j being Nat of F

hence ( len z = F