for K being Ring
for G, F being non empty right_complementable add-associative right_zeroed ModuleStr over K
for x being Vector of [:G,F:]
for x1 being Vector of G
for x2 being Vector of F st x = [x1,x2] holds
- x = [(- x1),(- x2)]