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 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 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 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
set such that A4:
(
v in the
carrier of
M &
x = Class R,
v )
by EQREL_1:def 5;
reconsider v =
v as
Element of
by A4;
y in Class R
;
then consider w being
set such that A5:
(
w in the
carrier of
M &
y = Class R,
w )
by EQREL_1:def 5;
reconsider w =
w as
Element of
by A5;
reconsider z =
Class R,
(v * w) as
Element of
X by A2, EQREL_1:def 5;
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 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 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 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 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 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 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 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 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 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 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 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 x' =
x as
Element of
Class R ;
assume A12:
y in Class R
;
b1 . x,y = b2 . x,y
then reconsider y' =
y as
Element of
Class R ;
consider v being
set such that A13:
(
v in the
carrier of
M &
x' = Class R,
v )
by A11, EQREL_1:def 5;
consider w being
set such that A14:
(
w in the
carrier of
M &
y' = Class R,
w )
by A12, EQREL_1:def 5;
reconsider v =
v,
w =
w as
Element of
by A13, A14;
b1 . x',
y' = 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 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 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 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