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) by Th7, A2, A3;
hence ( len z = F₁() + 1 & ( for j being Nat of F₁() holds z . j = F₃(j) ) ) by A1; :: thesis: verum