defpred S₁[ object , object ] means $2 = F₃($1);
A1: for x being object st x in NAT holds
ex y being object st S₁[x,y] ;
consider f being Function such that
A2: dom f = NAT and
A3: for x being object st x in NAT holds
S₁[x,f . x] from CLASSES1:sch 1(A1);

now :: thesis: for x being set st x in NAT holds
f . x is PartFunc of F₁(),F₂()

let x be set ; :: thesis: ( x in NAT implies f . x is PartFunc of F₁(),F₂() )
assume x in NAT ; :: thesis: f . x is PartFunc of F₁(),F₂()
then f . x = F₃(x) by A3;
hence f . x is PartFunc of F₁(),F₂() ; :: thesis: verum

end;

then reconsider f = f as Functional_Sequence of F₁(),F₂() by A2, Lm1;
take f ; :: thesis: for n being Nat holds f . n = F₃(n)
let n be Nat; :: thesis: f . n = F₃(n)
n in NAT by ORDINAL1:def 12;
hence f . n = F₃(n) by A3; :: thesis: verum