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) )

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

hence
Atlas w is associating
; :: thesis: verum
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;( (@ 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