consider z being XFinSequence such that
A1: len z = F₁() and
A2: for i being Nat st i in F₁() holds
z . i = F₃(i) from AFINSQ_1:sch 2();
for j being Nat st j in F₁() holds
z . j in F₂()

proof

let j be Nat; :: thesis: ( j in F₁() implies z . j in F₂() )
reconsider j0 = j as Element of NAT by ORDINAL1:def 12;
assume j in F₁() ; :: thesis: z . j in F₂()
then z . j0 = F₃(j0) by A2;
hence z . j in F₂() ; :: thesis: verum

end;

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