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

F_{4}(x,y) in F_{3}()
by A1;

consider f being PartFunc of [:F_{1}(),F_{2}():],F_{3}() such that

A3: ( ( for x, y being object holds

( [x,y] in dom f iff ( x in F_{1}() & y in F_{2}() & P_{1}[x,y] ) ) ) & ( for x, y being object st [x,y] in dom f holds

f . (x,y) = F_{4}(x,y) ) )
from BINOP_1:sch 7(A2);

take f ; :: thesis: ( ( for x being Element of F_{1}()

for y being Element of F_{2}() holds

( [x,y] in dom f iff P_{1}[x,y] ) ) & ( for x being Element of F_{1}()

for y being Element of F_{2}() st [x,y] in dom f holds

f . (x,y) = F_{4}(x,y) ) )

thus ( ( for x being Element of F_{1}()

for y being Element of F_{2}() holds

( [x,y] in dom f iff P_{1}[x,y] ) ) & ( for x being Element of F_{1}()

for y being Element of F_{2}() st [x,y] in dom f holds

f . (x,y) = F_{4}(x,y) ) )
by A3; :: thesis: verum

F

consider f being PartFunc of [:F

A3: ( ( for x, y being object holds

( [x,y] in dom f iff ( x in F

f . (x,y) = F

take f ; :: thesis: ( ( for x being Element of F

for y being Element of F

( [x,y] in dom f iff P

for y being Element of F

f . (x,y) = F

thus ( ( for x being Element of F

for y being Element of F

( [x,y] in dom f iff P

for y being Element of F

f . (x,y) = F