let G be non empty right_complementable Abelian add-associative right_zeroed midpoint_operator addLoopStr ; :: thesis: for M being non empty MidStr
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) = (a @ c) @ (b @ d)
let M be non empty MidStr ; :: 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) = (a @ c) @ (b @ d)
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) = (a @ c) @ (b @ d) )
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) = (a @ c) @ (b @ d)
let a, b, c, d be Point of M; :: thesis: (a @ b) @ (c @ d) = (a @ c) @ (b @ d)
A3: w . (b,(a @ b)) = w . (b,(b @ a)) by A1, A2, Th8
.= w . ((b @ a),a) by A2
.= w . ((a @ b),a) by A1, A2, Th8 ;
set p = (a @ b) @ (c @ d);
A4: w . (c,(c @ d)) = w . ((c @ d),d) by A2;
A5: w . (b,(b @ d)) = w . ((b @ d),d) by A2;
w . (c,(a @ c)) = w . (c,(c @ a)) by A1, A2, Th8
.= w . ((c @ a),a) by A2
.= w . ((a @ c),a) by A1, A2, Th8 ;
then Double (w . ((a @ c),(c @ d))) = w . (a,d) by A1, A4, Th14
.= - (w . (d,a)) by A1, Th4
.= - (Double (w . ((b @ d),(a @ b)))) by A1, A5, A3, Th14
.= Double (- (w . ((b @ d),(a @ b)))) by Th12
.= Double (w . ((a @ b),(b @ d))) by A1, Th4 ;
then w . ((a @ c),(c @ d)) = w . ((a @ b),(b @ d)) by Th17;
then A6: (w . ((a @ c),((a @ b) @ (c @ d)))) + (w . (((a @ b) @ (c @ d)),(c @ d))) = w . ((a @ b),(b @ d)) by A1
.= (w . (((a @ b) @ (c @ d)),(b @ d))) + (w . ((a @ b),((a @ b) @ (c @ d)))) by A1 ;
w . ((a @ b),((a @ b) @ (c @ d))) = w . (((a @ b) @ (c @ d)),(c @ d)) by A2;
then w . ((a @ c),((a @ b) @ (c @ d))) = w . (((a @ b) @ (c @ d)),(b @ d)) by A6, RLVECT_1:8;
hence (a @ b) @ (c @ d) = (a @ c) @ (b @ d) by A2; :: thesis: verum