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
object such that A2:
P in Loops a
and A3:
x = Class (
(EqRel (X,a)),
P)
by EQREL_1:def 3;
y in Class (EqRel (X,a))
;
then consider Q being
object such that A4:
Q in Loops a
and A5:
y = Class (
(EqRel (X,a)),
Q)
by EQREL_1:def 3;
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 3;
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
multMagma(# (Class (EqRel (X,a))),g #)
; ( the carrier of multMagma(# (Class (EqRel (X,a))),g #) = Class (EqRel (X,a)) & ( for x, y being Element of multMagma(# (Class (EqRel (X,a))),g #) ex P, Q being Loop of a st
( x = Class ((EqRel (X,a)),P) & y = Class ((EqRel (X,a)),Q) & the multF of multMagma(# (Class (EqRel (X,a))),g #) . (x,y) = Class ((EqRel (X,a)),(P + Q)) ) ) )
thus
( the carrier of multMagma(# (Class (EqRel (X,a))),g #) = Class (EqRel (X,a)) & ( for x, y being Element of multMagma(# (Class (EqRel (X,a))),g #) ex P, Q being Loop of a st
( x = Class ((EqRel (X,a)),P) & y = Class ((EqRel (X,a)),Q) & the multF of multMagma(# (Class (EqRel (X,a))),g #) . (x,y) = Class ((EqRel (X,a)),(P + Q)) ) ) )
by A6; verum