reconsider L1 = F₂() as Sequence by A1, ORDINAL1:def 7;
reconsider L2 = F₃() as Sequence by A2, ORDINAL1:def 7;
A3: ( dom L1 = NAT & ( for B being Ordinal
for T1 being Sequence st B in NAT & T1 = L1 | B holds
L1 . B = F₁(T1) ) ) by A1;
A4: ( dom L2 = NAT & ( for B being Ordinal
for T2 being Sequence st B in NAT & T2 = L2 | B holds
L2 . B = F₁(T2) ) ) by A2;
L1 = L2 from ORDINAL1:sch 3(A3, A4);
hence F₂() = F₃() ; :: thesis: verum