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;

take a ; :: thesis: w . (a,b) = x

w . (a,b) = - (- x) by A1, A2, Th4

.= x by RLVECT_1:17 ;

hence w . (a,b) = x ; :: thesis: verum

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;

take a ; :: thesis: w . (a,b) = x

w . (a,b) = - (- x) by A1, A2, Th4

.= x by RLVECT_1:17 ;

hence w . (a,b) = x ; :: thesis: verum