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