A1:
( not M is empty implies ex b being BinOp of (Class R) st
for x, y being Element of Class R
for v, w being Element of M st x = Class (R,v) & y = Class (R,w) holds
b . (x,y) = Class (R,(v * w)) )
proof
assume A2:
not
M is
empty
;
ex b being BinOp of (Class R) st
for x, y being Element of Class R
for v, w being Element of M st x = Class (R,v) & y = Class (R,w) holds
b . (x,y) = Class (R,(v * w))
then reconsider X =
Class R as non
empty set ;
defpred S1[
set ,
set ,
set ]
means for
x,
y being
Element of
Class R for
v,
w being
Element of
M st
x = $1 &
y = $2 &
x = Class (
R,
v) &
y = Class (
R,
w) holds
$3
= Class (
R,
(v * w));
A3:
for
x,
y being
Element of
X ex
z being
Element of
X st
S1[
x,
y,
z]
proof
let x,
y be
Element of
X;
ex z being Element of X st S1[x,y,z]
x in Class R
;
then consider v being
object such that A4:
(
v in the
carrier of
M &
x = Class (
R,
v) )
by EQREL_1:def 3;
reconsider v =
v as
Element of
M by A4;
y in Class R
;
then consider w being
object such that A5:
(
w in the
carrier of
M &
y = Class (
R,
w) )
by EQREL_1:def 3;
reconsider w =
w as
Element of
M by A5;
reconsider z =
Class (
R,
(v * w)) as
Element of
X by A2, EQREL_1:def 3;
take
z
;
S1[x,y,z]
thus
S1[
x,
y,
z]
by A4, A5, Th2;
verum
end;
consider b being
Function of
[:X,X:],
X such that A6:
for
x,
y being
Element of
X holds
S1[
x,
y,
b . (
x,
y)]
from BINOP_1:sch 3(A3);
reconsider b =
b as
BinOp of
(Class R) ;
take
b
;
for x, y being Element of Class R
for v, w being Element of M st x = Class (R,v) & y = Class (R,w) holds
b . (x,y) = Class (R,(v * w))
thus
for
x,
y being
Element of
Class R for
v,
w being
Element of
M st
x = Class (
R,
v) &
y = Class (
R,
w) holds
b . (
x,
y)
= Class (
R,
(v * w))
by A6;
verum
end;
A7:
( M is empty implies ex b being BinOp of (Class R) st b = {} )
for b1, b2 being BinOp of (Class R) st not M is empty & ( for x, y being Element of Class R
for v, w being Element of M st x = Class (R,v) & y = Class (R,w) holds
b1 . (x,y) = Class (R,(v * w)) ) & ( for x, y being Element of Class R
for v, w being Element of M st x = Class (R,v) & y = Class (R,w) holds
b2 . (x,y) = Class (R,(v * w)) ) holds
b1 = b2
proof
let b1,
b2 be
BinOp of
(Class R);
( not M is empty & ( for x, y being Element of Class R
for v, w being Element of M st x = Class (R,v) & y = Class (R,w) holds
b1 . (x,y) = Class (R,(v * w)) ) & ( for x, y being Element of Class R
for v, w being Element of M st x = Class (R,v) & y = Class (R,w) holds
b2 . (x,y) = Class (R,(v * w)) ) implies b1 = b2 )
assume
not
M is
empty
;
( ex x, y being Element of Class R ex v, w being Element of M st
( x = Class (R,v) & y = Class (R,w) & not b1 . (x,y) = Class (R,(v * w)) ) or ex x, y being Element of Class R ex v, w being Element of M st
( x = Class (R,v) & y = Class (R,w) & not b2 . (x,y) = Class (R,(v * w)) ) or b1 = b2 )
assume A9:
for
x,
y being
Element of
Class R for
v,
w being
Element of
M st
x = Class (
R,
v) &
y = Class (
R,
w) holds
b1 . (
x,
y)
= Class (
R,
(v * w))
;
( ex x, y being Element of Class R ex v, w being Element of M st
( x = Class (R,v) & y = Class (R,w) & not b2 . (x,y) = Class (R,(v * w)) ) or b1 = b2 )
assume A10:
for
x,
y being
Element of
Class R for
v,
w being
Element of
M st
x = Class (
R,
v) &
y = Class (
R,
w) holds
b2 . (
x,
y)
= Class (
R,
(v * w))
;
b1 = b2
for
x,
y being
set st
x in Class R &
y in Class R holds
b1 . (
x,
y)
= b2 . (
x,
y)
proof
let x,
y be
set ;
( x in Class R & y in Class R implies b1 . (x,y) = b2 . (x,y) )
assume A11:
x in Class R
;
( not y in Class R or b1 . (x,y) = b2 . (x,y) )
then reconsider x9 =
x as
Element of
Class R ;
assume A12:
y in Class R
;
b1 . (x,y) = b2 . (x,y)
then reconsider y9 =
y as
Element of
Class R ;
consider v being
object such that A13:
(
v in the
carrier of
M &
x9 = Class (
R,
v) )
by A11, EQREL_1:def 3;
consider w being
object such that A14:
(
w in the
carrier of
M &
y9 = Class (
R,
w) )
by A12, EQREL_1:def 3;
reconsider v =
v,
w =
w as
Element of
M by A13, A14;
b1 . (
x9,
y9)
= Class (
R,
(v * w))
by A13, A14, A9;
hence
b1 . (
x,
y)
= b2 . (
x,
y)
by A13, A14, A10;
verum
end;
hence
b1 = b2
by BINOP_1:1;
verum
end;
hence
( ( for b1 being BinOp of (Class R) holds verum ) & ( not M is empty implies ex b1 being BinOp of (Class R) st
for x, y being Element of Class R
for v, w being Element of M st x = Class (R,v) & y = Class (R,w) holds
b1 . (x,y) = Class (R,(v * w)) ) & ( M is empty implies ex b1 being BinOp of (Class R) st b1 = {} ) & ( for b1, b2 being BinOp of (Class R) holds
( ( not M is empty & ( for x, y being Element of Class R
for v, w being Element of M st x = Class (R,v) & y = Class (R,w) holds
b1 . (x,y) = Class (R,(v * w)) ) & ( for x, y being Element of Class R
for v, w being Element of M st x = Class (R,v) & y = Class (R,w) holds
b2 . (x,y) = Class (R,(v * w)) ) implies b1 = b2 ) & ( M is empty & b1 = {} & b2 = {} implies b1 = b2 ) ) ) )
by A1, A7; verum