A2:
for x, y being object st x in F_{1}() & y in F_{2}() holds

ex z being object st

( z in F_{3}() & P_{1}[x,y,z] )
_{1}(),F_{2}():],F_{3}() such that

A5: for x, y being object st x in F_{1}() & y in F_{2}() holds

P_{1}[x,y,f . (x,y)]
from BINOP_1:sch 1(A2);

take f ; :: thesis: for x, y being set st x in F_{1}() & y in F_{2}() holds

P_{1}[x,y,f . (x,y)]

thus for x, y being set st x in F_{1}() & y in F_{2}() holds

P_{1}[x,y,f . (x,y)]
by A5; :: thesis: verum

ex z being object st

( z in F

proof

consider f being Function of [:F
let x, y be object ; :: thesis: ( x in F_{1}() & y in F_{2}() implies ex z being object st

( z in F_{3}() & P_{1}[x,y,z] ) )

assume A3: ( x in F_{1}() & y in F_{2}() )
; :: thesis: ex z being object st

( z in F_{3}() & P_{1}[x,y,z] )

reconsider x = x, y = y as set by TARSKI:1;

consider z being set such that

A4: ( z in F_{3}() & P_{1}[x,y,z] )
by A3, A1;

take z ; :: thesis: ( z in F_{3}() & P_{1}[x,y,z] )

( z in F_{3}() & P_{1}[x,y,z] )
by A4;

hence ( z in F_{3}() & P_{1}[x,y,z] )
; :: thesis: verum

end;( z in F

assume A3: ( x in F

( z in F

reconsider x = x, y = y as set by TARSKI:1;

consider z being set such that

A4: ( z in F

take z ; :: thesis: ( z in F

( z in F

hence ( z in F

A5: for x, y being object st x in F

P

take f ; :: thesis: for x, y being set st x in F

P

thus for x, y being set st x in F

P