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, b9, c, c9 being Element of S st w . a,b = w . b,c & w . a,b9 = w . b9,c9 holds
w . c,c9 = Double (w . b,b9)
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, b9, c, c9 being Element of S st w . a,b = w . b,c & w . a,b9 = w . b9,c9 holds
w . c,c9 = Double (w . b,b9)
let w be Function of [:S,S:],the carrier of G; :: thesis: ( w is_atlas_of S,G implies for a, b, b9, c, c9 being Element of S st w . a,b = w . b,c & w . a,b9 = w . b9,c9 holds
w . c,c9 = Double (w . b,b9) )
assume A1: w is_atlas_of S,G ; :: thesis: for a, b, b9, c, c9 being Element of S st w . a,b = w . b,c & w . a,b9 = w . b9,c9 holds
w . c,c9 = Double (w . b,b9)
let a, b, b9, c, c9 be Element of S; :: thesis: ( w . a,b = w . b,c & w . a,b9 = w . b9,c9 implies w . c,c9 = Double (w . b,b9) )
assume A2: ( w . a,b = w . b,c & w . a,b9 = w . b9,c9 ) ; :: thesis: w . c,c9 = Double (w . b,b9)
thus w . c,c9 = (w . c,b9) + (w . b9,c9) by A1, Def3
.= ((w . c,a) + (w . a,b9)) + (w . b9,c9) by A1, Def3
.= (((w . c,b) + (w . b,a)) + (w . a,b9)) + (w . b9,c9) by A1, Def3
.= ((Double (w . b,a)) + (w . a,b9)) + (w . a,b9) by A1, A2, Th7
.= (Double (w . b,a)) + (Double (w . a,b9)) by RLVECT_1:def 6
.= Double ((w . b,a) + (w . a,b9)) by Th13
.= Double (w . b,b9) by A1, Def3 ; :: thesis: verum