let M be non empty MidStr ; :: thesis: for G being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for w being Function of [:the carrier of M,the carrier of M:],the carrier of G st w is_atlas_of the carrier of M,G & M,G are_associated_wrp w holds
for a, b, c, d being Point of M holds
( a @ b = c @ d iff w . a,d = w . c,b )
let G be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; :: thesis: for w being Function of [:the carrier of M,the carrier of M:],the carrier of G st w is_atlas_of the carrier of M,G & M,G are_associated_wrp w holds
for a, b, c, d being Point of M holds
( a @ b = c @ d iff w . a,d = w . c,b )
let w be Function of [:the carrier of M,the carrier of M:],the carrier of G; :: thesis: ( w is_atlas_of the carrier of M,G & M,G are_associated_wrp w implies for a, b, c, d being Point of M holds
( a @ b = c @ d iff w . a,d = w . c,b ) )
assume that
A1:
w is_atlas_of the carrier of M,G
and
A2:
M,G are_associated_wrp w
; :: thesis: for a, b, c, d being Point of M holds
( a @ b = c @ d iff w . a,d = w . c,b )
let a, b, c, d be Point of M; :: thesis: ( a @ b = c @ d iff w . a,d = w . c,b )
thus
( a @ b = c @ d implies w . a,d = w . c,b )
:: thesis: ( w . a,d = w . c,b implies a @ b = c @ d )proof
assume A3:
a @ b = c @ d
;
:: thesis: w . a,d = w . c,b
set p =
a @ b;
(
w . a,
(a @ b) = w . (a @ b),
b &
w . c,
(a @ b) = w . (a @ b),
d )
by A2, A3, Def2;
hence w . a,
d =
(w . c,(a @ b)) + (w . (a @ b),b)
by A1, Def3
.=
w . c,
b
by A1, Def3
;
:: thesis: verum
end;
thus
( w . a,d = w . c,b implies a @ b = c @ d )
:: thesis: verumproof
assume A4:
w . a,
d = w . c,
b
;
:: thesis: a @ b = c @ d
set p =
a @ b;
(w . (a @ b),b) + (w . (a @ b),d) =
(w . a,(a @ b)) + (w . (a @ b),d)
by A2, Def2
.=
w . a,
d
by A1, Def3
.=
(w . (a @ b),b) + (w . c,(a @ b))
by A1, A4, Def3
;
then
w . (a @ b),
d = w . c,
(a @ b)
by RLVECT_1:21;
hence
a @ b = c @ d
by A2, Def2;
:: thesis: verum
end;