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 ; :: thesis: 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 S₁[ 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 S₁[x,y,z]

proof

let x, y be Element of X; :: thesis: ex z being Element of X st S₁[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 ; :: thesis: S₁[x,y,z]
thus S₁[x,y,z] by A4, A5, Th2; :: thesis: verum

end;

consider b being Function of [:X,X:],X such that
A6: for x, y being Element of X holds S₁[x,y,b . (x,y)] from BINOP_1:sch 3(A3);
reconsider b = b as BinOp of (Class R) ;
take b ; :: thesis: 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; :: thesis: verum

end;

A7: ( M is empty implies ex b being BinOp of (Class R) st b = {} )

proof

assume M is empty ; :: thesis: ex b being BinOp of (Class R) st b = {}
then the carrier of M is empty ;
then A8: Class R is empty ;
set b = the BinOp of (Class R);
take the BinOp of (Class R) ; :: thesis: the BinOp of (Class R) = {}
thus the BinOp of (Class R) = {} by A8; :: thesis: verum

end;

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); :: thesis: ( 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 ; :: thesis: ( 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)) ; :: thesis: ( 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)) ; :: thesis: 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 ; :: thesis: ( x in Class R & y in Class R implies b1 . (x,y) = b2 . (x,y) )
assume A11: x in Class R ; :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum

end;

hence b1 = b2 by BINOP_1:1; :: thesis: verum

end;

hence ( ( for b₁ being BinOp of (Class R) holds verum ) & ( 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)) ) & ( M is empty implies ex b₁ being BinOp of (Class R) st b₁ = {} ) & ( for b₁, b₂ 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
b₁ . (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
b₂ . (x,y) = Class (R,(v * w)) ) implies b₁ = b₂ ) & ( M is empty & b₁ = {} & b₂ = {} implies b₁ = b₂ ) ) ) ) by A1, A7; :: thesis: verum