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