let S be non empty set ; :: thesis: for G being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for w being Function of [:S,S:],the carrier of G st w is_atlas_of S,G holds
for a, b, b', c, c' being Element of S st w . a,b = w . b,c & w . a,b' = w . b',c' holds
w . c,c' = Double (w . b,b')
let G be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; :: thesis: for w being Function of [:S,S:],the carrier of G st w is_atlas_of S,G holds
for a, b, b', c, c' being Element of S st w . a,b = w . b,c & w . a,b' = w . b',c' holds
w . c,c' = Double (w . b,b')
let w be Function of [:S,S:],the carrier of G; :: thesis: ( w is_atlas_of S,G implies for a, b, b', c, c' being Element of S st w . a,b = w . b,c & w . a,b' = w . b',c' holds
w . c,c' = Double (w . b,b') )
assume A1: w is_atlas_of S,G ; :: thesis: for a, b, b', c, c' being Element of S st w . a,b = w . b,c & w . a,b' = w . b',c' holds
w . c,c' = Double (w . b,b')
let a, b, b', c, c' be Element of S; :: thesis: ( w . a,b = w . b,c & w . a,b' = w . b',c' implies w . c,c' = Double (w . b,b') )
assume A2: ( w . a,b = w . b,c & w . a,b' = w . b',c' ) ; :: thesis: w . c,c' = Double (w . b,b')
thus w . c,c' = (w . c,b') + (w . b',c') by A1, Def3
.= ((w . c,a) + (w . a,b')) + (w . b',c') by A1, Def3
.= (((w . c,b) + (w . b,a)) + (w . a,b')) + (w . b',c') by A1, Def3
.= ((Double (w . b,a)) + (w . a,b')) + (w . a,b') by A1, A2, Th7
.= (Double (w . b,a)) + (Double (w . a,b')) by RLVECT_1:def 6
.= Double ((w . b,a) + (w . a,b')) by Th13
.= Double (w . b,b') by A1, Def3 ; :: thesis: verum