set A = Class (EqRel X,a);
defpred S1[ set , set , set ] means ex P, Q being Loop of a st
( $1 = Class (EqRel X,a),P & $2 = Class (EqRel X,a),Q & $3 = Class (EqRel X,a),(P + Q) );
A1:
for x, y being Element of Class (EqRel X,a) ex z being Element of Class (EqRel X,a) st S1[x,y,z]
proof
let x,
y be
Element of
Class (EqRel X,a);
:: thesis: ex z being Element of Class (EqRel X,a) st S1[x,y,z]
x in Class (EqRel X,a)
;
then consider P being
set such that A2:
P in Loops a
and A3:
x = Class (EqRel X,a),
P
by EQREL_1:def 5;
y in Class (EqRel X,a)
;
then consider Q being
set such that A4:
Q in Loops a
and A5:
y = Class (EqRel X,a),
Q
by EQREL_1:def 5;
reconsider P =
P,
Q =
Q as
Loop of
a by A2, A4, Def1;
P + Q in Loops a
by Def1;
then reconsider z =
Class (EqRel X,a),
(P + Q) as
Element of
Class (EqRel X,a) by EQREL_1:def 5;
take
z
;
:: thesis: S1[x,y,z]
thus
S1[
x,
y,
z]
by A3, A5;
:: thesis: verum
end;
consider g being BinOp of (Class (EqRel X,a)) such that
A6:
for a, b being Element of Class (EqRel X,a) holds S1[a,b,g . a,b]
from BINOP_1:sch 3(A1);
take G = multMagma(# (Class (EqRel X,a)),g #); :: thesis: ( the carrier of G = Class (EqRel X,a) & ( for x, y being Element of G ex P, Q being Loop of a st
( x = Class (EqRel X,a),P & y = Class (EqRel X,a),Q & the multF of G . x,y = Class (EqRel X,a),(P + Q) ) ) )
thus
( the carrier of G = Class (EqRel X,a) & ( for x, y being Element of G ex P, Q being Loop of a st
( x = Class (EqRel X,a),P & y = Class (EqRel X,a),Q & the multF of G . x,y = Class (EqRel X,a),(P + Q) ) ) )
by A6; :: thesis: verum