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);
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
;
S1[x,y,z]
thus
S1[
x,
y,
z]
by A3, A5;
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 #); ( 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; verum