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 & M,G are_associated_wrp w 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 & M,G are_associated_wrp w 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 & M,G are_associated_wrp w implies for a, b, c, d being Point of M holds (a @ b) @ (c @ d) = (a @ c) @ (b @ d) )
assume A1: ( w is_atlas_of the carrier of M,G & M,G are_associated_wrp w ) ; :: 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)
set p = (a @ b) @ (c @ d);
A2: w . (a @ b),((a @ b) @ (c @ d)) = w . ((a @ b) @ (c @ d)),(c @ d) by A1, Def2;
A3: w . c,(a @ c) = w . c,(c @ a) by A1, Th10
.= w . (c @ a),a by A1, Def2
.= w . (a @ c),a by A1, Th10 ;
A4: w . c,(c @ d) = w . (c @ d),d by A1, Def2;
A5: w . b,(b @ d) = w . (b @ d),d by A1, Def2;
A6: w . b,(a @ b) = w . b,(b @ a) by A1, Th10
.= w . (b @ a),a by A1, Def2
.= w . (a @ b),a by A1, Th10 ;
Double (w . (a @ c),(c @ d)) = w . a,d by A1, A3, A4, Th17
.= - (w . d,a) by A1, Th6
.= - (Double (w . (b @ d),(a @ b))) by A1, A5, A6, Th17
.= Double (- (w . (b @ d),(a @ b))) by Th15
.= Double (w . (a @ b),(b @ d)) by A1, Th6 ;
then w . (a @ c),(c @ d) = w . (a @ b),(b @ d) by Th20;
then (w . (a @ c),((a @ b) @ (c @ d))) + (w . ((a @ b) @ (c @ d)),(c @ d)) = w . (a @ b),(b @ d) by A1, Def3
.= (w . ((a @ b) @ (c @ d)),(b @ d)) + (w . (a @ b),((a @ b) @ (c @ d))) by A1, Def3 ;
then w . (a @ c),((a @ b) @ (c @ d)) = w . ((a @ b) @ (c @ d)),(b @ d) by A2, RLVECT_1:21;
hence (a @ b) @ (c @ d) = (a @ c) @ (b @ d) by A1, Def2; :: thesis: verum