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

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