consider z being FinSequence such that
A1: len z = F₁() and
A2: for i being Nat st i in dom z holds
z . i = F₃(i) from FINSEQ_1:sch 2();
A3: Seg F₁() = dom z by A1, FINSEQ_1:def 3;
for j being Nat st j in Seg F₁() holds
z . j in F₂()

proof

let j be Nat; :: thesis: ( j in Seg F₁() implies z . j in F₂() )
assume j in Seg F₁() ; :: thesis: z . j in F₂()
then z . j = F₃(j) by A2, A3;
hence z . j in F₂() ; :: thesis: verum

end;

then reconsider z = z as FinSequence of F₂() by A3, Th10;
take z ; :: thesis: ( len z = F₁() & ( for j being Nat st j in dom z holds
z . j = F₃(j) ) )
thus len z = F₁() by A1; :: thesis: for j being Nat st j in dom z holds
z . j = F₃(j)
let j be Nat; :: thesis: ( j in dom z implies z . j = F₃(j) )
thus ( j in dom z implies z . j = F₃(j) ) by A2; :: thesis: verum