defpred S1[ object , object , object ] means ( P1[$1,$2] & $3 = F4($1,$2) );
A2:
for x, y, z1, z2 being object st x in F1() & y in F2() & S1[x,y,z1] & S1[x,y,z2] holds
z1 = z2
;
A3:
for x, y, z being object st x in F1() & y in F2() & S1[x,y,z] holds
z in F3()
by A1;
consider f being PartFunc of [:F1(),F2():],F3() such that
A4:
for x, y being object holds
( [x,y] in dom f iff ( x in F1() & y in F2() & ex z being object st S1[x,y,z] ) )
and
A5:
for x, y being object st [x,y] in dom f holds
S1[x,y,f . (x,y)]
from BINOP_1:sch 5(A3, A2);
take
f
; ( ( for x, y being object holds
( [x,y] in dom f iff ( x in F1() & y in F2() & P1[x,y] ) ) ) & ( for x, y being object st [x,y] in dom f holds
f . (x,y) = F4(x,y) ) )
thus
for x, y being object holds
( [x,y] in dom f iff ( x in F1() & y in F2() & P1[x,y] ) )
for x, y being object st [x,y] in dom f holds
f . (x,y) = F4(x,y)proof
let x,
y be
object ;
( [x,y] in dom f iff ( x in F1() & y in F2() & P1[x,y] ) )
thus
(
[x,y] in dom f implies (
x in F1() &
y in F2() &
P1[
x,
y] ) )
( x in F1() & y in F2() & P1[x,y] implies [x,y] in dom f )proof
assume A6:
[x,y] in dom f
;
( x in F1() & y in F2() & P1[x,y] )
then
ex
z being
object st
(
P1[
x,
y] &
z = F4(
x,
y) )
by A4;
hence
(
x in F1() &
y in F2() &
P1[
x,
y] )
by A4, A6;
verum
end;
assume that A7:
(
x in F1() &
y in F2() )
and A8:
P1[
x,
y]
;
[x,y] in dom f
ex
z being
object st
(
P1[
x,
y] &
z = F4(
x,
y) )
by A8;
hence
[x,y] in dom f
by A4, A7;
verum
end;
thus
for x, y being object st [x,y] in dom f holds
f . (x,y) = F4(x,y)
by A5; verum