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 & w is associating 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 & w is associating 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 & w is associating 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: w is associating ; :: 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 )

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 & w is associating 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 & w is associating 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 & w is associating 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: w is associating ; :: 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

thus
( w . (a,d) = w . (c,b) implies a @ b = c @ d )
:: thesis: verum
set p = a @ b;

assume a @ b = c @ d ; :: thesis: w . (a,d) = w . (c,b)

then A3: w . (c,(a @ b)) = w . ((a @ b),d) by A2;

w . (a,(a @ b)) = w . ((a @ b),b) by A2;

hence w . (a,d) = (w . (c,(a @ b))) + (w . ((a @ b),b)) by A1, A3

.= w . (c,b) by A1 ;

:: thesis: verum

end;assume a @ b = c @ d ; :: thesis: w . (a,d) = w . (c,b)

then A3: w . (c,(a @ b)) = w . ((a @ b),d) by A2;

w . (a,(a @ b)) = w . ((a @ b),b) by A2;

hence w . (a,d) = (w . (c,(a @ b))) + (w . ((a @ b),b)) by A1, A3

.= w . (c,b) by A1 ;

:: thesis: verum

proof

set p = a @ b;

assume A4: w . (a,d) = w . (c,b) ; :: thesis: a @ b = c @ d

(w . ((a @ b),b)) + (w . ((a @ b),d)) = (w . (a,(a @ b))) + (w . ((a @ b),d)) by A2

.= w . (a,d) by A1

.= (w . ((a @ b),b)) + (w . (c,(a @ b))) by A1, A4 ;

then w . ((a @ b),d) = w . (c,(a @ b)) by RLVECT_1:8;

hence a @ b = c @ d by A2; :: thesis: verum

end;assume A4: w . (a,d) = w . (c,b) ; :: thesis: a @ b = c @ d

(w . ((a @ b),b)) + (w . ((a @ b),d)) = (w . (a,(a @ b))) + (w . ((a @ b),d)) by A2

.= w . (a,d) by A1

.= (w . ((a @ b),b)) + (w . (c,(a @ b))) by A1, A4 ;

then w . ((a @ b),d) = w . (c,(a @ b)) by RLVECT_1:8;

hence a @ b = c @ d by A2; :: thesis: verum