defpred S1[ set , set , set ] means ex x9, y9 being Element of n -tuples_on D st
( $1 = x9 & $2 = y9 & $3 = F .: (x9,y9) );
A1:
for x, y being Element of n -tuples_on D ex z being Element of n -tuples_on D st S1[x,y,z]
proof
let x,
y be
Element of
n -tuples_on D;
ex z being Element of n -tuples_on D st S1[x,y,z]
reconsider x9 =
x,
y9 =
y as
Element of
n -tuples_on D ;
reconsider z =
F .: (
x9,
y9) as
Element of
n -tuples_on D ;
take
z
;
S1[x,y,z]
take
x9
;
ex y9 being Element of n -tuples_on D st
( x = x9 & y = y9 & z = F .: (x9,y9) )
take
y9
;
( x = x9 & y = y9 & z = F .: (x9,y9) )
thus
(
x = x9 &
y = y9 &
z = F .: (
x9,
y9) )
;
verum
end;
consider G being BinOp of (n -tuples_on D) such that
A2:
for x, y being Element of n -tuples_on D holds S1[x,y,G . (x,y)]
from BINOP_1:sch 3(A1);
take
G
; for x, y being Element of n -tuples_on D holds G . (x,y) = F .: (x,y)
let p1, p2 be Element of n -tuples_on D; G . (p1,p2) = F .: (p1,p2)
reconsider x = p1, y = p2 as Element of n -tuples_on D ;
ex x9, y9 being Element of n -tuples_on D st
( x = x9 & y = y9 & G . (x,y) = F .: (x9,y9) )
by A2;
hence
G . (p1,p2) = F .: (p1,p2)
; verum