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
.= ((w . (c,a)) + (w . (a,b9))) + (w . (b9,c9)) by A1
.= (((w . (c,b)) + (w . (b,a))) + (w . (a,b9))) + (w . (b9,c9)) by A1
.= ((Double (w . (b,a))) + (w . (a,b9))) + (w . (a,b9)) by A1, A2, Th5
.= (Double (w . (b,a))) + (Double (w . (a,b9))) by RLVECT_1:def 3
.= Double ((w . (b,a)) + (w . (a,b9))) by Th10
.= Double (w . (b,b9)) by A1 ; :: thesis: verum