A2:
for x, y being object st x in F1() & y in F2() holds
ex z being object st
( z in F3() & P1[x,y,z] )
proof
let x,
y be
object ;
( x in F1() & y in F2() implies ex z being object st
( z in F3() & P1[x,y,z] ) )
assume A3:
(
x in F1() &
y in F2() )
;
ex z being object st
( z in F3() & P1[x,y,z] )
reconsider x =
x,
y =
y as
set by TARSKI:1;
consider z being
set such that A4:
(
z in F3() &
P1[
x,
y,
z] )
by A3, A1;
take
z
;
( z in F3() & P1[x,y,z] )
(
z in F3() &
P1[
x,
y,
z] )
by A4;
hence
(
z in F3() &
P1[
x,
y,
z] )
;
verum
end;
consider f being Function of [:F1(),F2():],F3() such that
A5:
for x, y being object st x in F1() & y in F2() holds
P1[x,y,f . (x,y)]
from BINOP_1:sch 1(A2);
take
f
; for x, y being set st x in F1() & y in F2() holds
P1[x,y,f . (x,y)]
thus
for x, y being set st x in F1() & y in F2() holds
P1[x,y,f . (x,y)]
by A5; verum