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