let S be non empty set ; :: thesis: for G being non empty right_complementable 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 b being Element of S
for x being Element of G ex a being Element of S st w . a,b = x
let G be non empty right_complementable 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 b being Element of S
for x being Element of G ex a being Element of S st w . a,b = x
let w be Function of [:S,S:],the carrier of G; :: thesis: ( w is_atlas_of S,G implies for b being Element of S
for x being Element of G ex a being Element of S st w . a,b = x )
assume A1: w is_atlas_of S,G ; :: thesis: for b being Element of S
for x being Element of G ex a being Element of S st w . a,b = x
let b be Element of S; :: thesis: for x being Element of G ex a being Element of S st w . a,b = x
let x be Element of G; :: thesis: ex a being Element of S st w . a,b = x
consider a being Element of S such that
A2: w . b,a = - x by A1, Def3;
take a ; :: thesis: w . a,b = x
w . a,b = - (- x) by A1, A2, Th6
.= x by RLVECT_1:30 ;
hence w . a,b = x ; :: thesis: verum