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