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
MidStr(# S,(@ w) #),G are_associated_wrp Atlas w
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
MidStr(# S,(@ w) #),G are_associated_wrp Atlas w
let w be Function of [:S,S:],the carrier of G; :: thesis: ( w is_atlas_of S,G implies MidStr(# S,(@ w) #),G are_associated_wrp Atlas w )
assume w is_atlas_of S,G ; :: thesis: MidStr(# S,(@ w) #),G are_associated_wrp Atlas w
then for a, b, c being Point of MidStr(# S,(@ w) #) holds
( a @ b = c iff (Atlas w) . a,c = (Atlas w) . c,b ) by Lm2;
hence MidStr(# S,(@ w) #),G are_associated_wrp Atlas w by Def2; :: thesis: verum