A2:
for x being Element of NAT
for y being Element of F1() ex z being Element of F2() st P1[x,y,z]
by A1;
consider f being Function of [:NAT,F1():],F2() such that
A3:
for x being Element of NAT
for y being Element of F1() holds P1[x,y,f . (x,y)]
from BINOP_1:sch 3(A2);
take
f
; for x being Nat
for y being Element of F1() holds P1[x,y,f . (x,y)]
let x be Nat; for y being Element of F1() holds P1[x,y,f . (x,y)]
let y be Element of F1(); P1[x,y,f . (x,y)]
x in NAT
by ORDINAL1:def 12;
hence
P1[x,y,f . (x,y)]
by A3; verum