defpred S_{1}[ object , object ] means ( $1 in F_{1}() & $2 in F_{2}() & P_{1}[$1,$2] );

A2: for x, y being object st S_{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}() & S_{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 6(A2);

take f ; :: thesis: ( ( 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) ) )

thus ( ( 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) ) )
by A3; :: thesis: verum

A2: for x, y being object st S

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, y being object holds

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

f . (x,y) = F

thus ( ( for x, y being object holds

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

f . (x,y) = F