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

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

z1 = z2 ;

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

z in F_{3}()
by A1;

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

A4: for x, y being object holds

( [x,y] in dom f iff ( x in F_{1}() & y in F_{2}() & ex z being object st S_{1}[x,y,z] ) )
and

A5: for x, y being object st [x,y] in dom f holds

S_{1}[x,y,f . (x,y)]
from BINOP_1:sch 5(A3, 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] ) )
:: thesis: for x, y being object st [x,y] in dom f holds

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

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

A2: for x, y, z1, z2 being object st x in F

z1 = z2 ;

A3: for x, y, z being object st x in F

z in F

consider f being PartFunc of [:F

A4: for x, y being object holds

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

A5: for x, y being object st [x,y] in dom f holds

S

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

proof

thus
for x, y being object st [x,y] in dom f holds
let x, y be object ; :: thesis: ( [x,y] in dom f iff ( x in F_{1}() & y in F_{2}() & P_{1}[x,y] ) )

thus ( [x,y] in dom f implies ( x in F_{1}() & y in F_{2}() & P_{1}[x,y] ) )
:: thesis: ( x in F_{1}() & y in F_{2}() & P_{1}[x,y] implies [x,y] in dom f )

A7: ( x in F_{1}() & y in F_{2}() )
and

A8: P_{1}[x,y]
; :: thesis: [x,y] in dom f

ex z being object st

( P_{1}[x,y] & z = F_{4}(x,y) )
by A8;

hence [x,y] in dom f by A4, A7; :: thesis: verum

end;thus ( [x,y] in dom f implies ( x in F

proof

assume that
assume A6:
[x,y] in dom f
; :: thesis: ( x in F_{1}() & y in F_{2}() & P_{1}[x,y] )

then ex z being object st

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

hence ( x in F_{1}() & y in F_{2}() & P_{1}[x,y] )
by A4, A6; :: thesis: verum

end;then ex z being object st

( P

hence ( x in F

A7: ( x in F

A8: P

ex z being object st

( P

hence [x,y] in dom f by A4, A7; :: thesis: verum

f . (x,y) = F