reconsider S = Seg (F₁() + 1) as non empty set by FINSEQ_1:4;
consider z being FinSequence of F₂() such that
A1: len z = F₁() + 1 and
A2: for j being Nat st j in dom z holds
z . j = F₃(j) from FINSEQ_2:sch 1();
take z ; :: thesis: ( len z = F₁() + 1 & ( for j being Nat of F₁() holds z . j = F₃(j) ) )
A3: dom z = Seg (F₁() + 1) by A1, FINSEQ_1:def 3;
for j being Nat of F₁() holds z . j = F₃(j)

proof

let j be Nat of F₁(); :: thesis: z . j = F₃(j)
j in S by Th8;
hence z . j = F₃(j) by A2, A3; :: thesis: verum

end;

hence ( len z = F₁() + 1 & ( for j being Nat of F₁() holds z . j = F₃(j) ) ) by A1; :: thesis: verum