let S be non empty set ; :: thesis: for G being non empty right_complementable Abelian add-associative right_zeroed midpoint_operator addLoopStr
for w being Function of [:S,S:], the carrier of G st w is_atlas_of S,G holds
Atlas w is associating
let G be non empty right_complementable Abelian add-associative right_zeroed midpoint_operator addLoopStr ; :: thesis: for w being Function of [:S,S:], the carrier of G st w is_atlas_of S,G holds
Atlas w is associating
let w be Function of [:S,S:], the carrier of G; :: thesis: ( w is_atlas_of S,G implies Atlas w is associating )
assume A1: w is_atlas_of S,G ; :: thesis: Atlas w is associating
for a, b, c being Point of MidStr(# S,(@ w) #) holds
( a @ b = c iff (Atlas w) . (a,c) = (Atlas w) . (c,b) )

proof

let a, b, c be Point of MidStr(# S,(@ w) #); :: thesis: ( a @ b = c iff (Atlas w) . (a,c) = (Atlas w) . (c,b) )
( (@ w) . (a,b) = c iff w . (a,c) = w . (c,b) ) by A1, Th24;
hence ( a @ b = c iff (Atlas w) . (a,c) = (Atlas w) . (c,b) ) by MIDSP_1:def 1; :: thesis: verum

end;

hence Atlas w is associating ; :: thesis: verum