let N be non empty ConjNormAlgStr ; :: thesis: for a being Element of N st N is well-conjugated & N is reflexive & N is discerning & N is RealNormSpace-like & N is vector-distributive & N is scalar-distributive & N is scalar-associative & N is scalar-unital & N is Abelian & N is add-associative & N is right_zeroed & N is right_complementable & N is associative & N is distributive & N is well-unital & not N is degenerated & N is almost_left_invertible holds
(- a) *' = - (a *')
let a be Element of N; :: thesis: ( N is well-conjugated & N is reflexive & N is discerning & N is RealNormSpace-like & N is vector-distributive & N is scalar-distributive & N is scalar-associative & N is scalar-unital & N is Abelian & N is add-associative & N is right_zeroed & N is right_complementable & N is associative & N is distributive & N is well-unital & not N is degenerated & N is almost_left_invertible implies (- a) *' = - (a *') )
assume that
A1: N is well-conjugated and
A2: ( N is reflexive & N is discerning & N is RealNormSpace-like & N is vector-distributive & N is scalar-distributive & N is scalar-associative & N is scalar-unital & N is Abelian & N is add-associative & N is right_zeroed & N is right_complementable ) and
A3: N is associative and
A4: N is distributive and
A5: N is well-unital and
A6: ( not N is degenerated & N is almost_left_invertible ) ; :: thesis: (- a) *' = - (a *')

per cases ( not a is zero or a is zero ) ;

suppose A7: not a is zero ; :: thesis: (- a) *' = - (a *')

then A8: (a *') * a = (||.a.|| ^2) * (1. N) by A1, Def3;
A9: ((- a) *') * (- a) = (||.(- a).|| ^2) * (1. N) by A1, A2, A6, A7, Def3;
A10: ||.(- a).|| = ||.a.|| by A2, NORMSP_1:2;
A11: a <> 0. N by A7;
A12: a * (/ a) = 1. N by A2, A3, A4, A5, A6, A11, VECTSP_2:9;
then A13: (- a) * (- (/ a)) = 1. N by A2, A4, VECTSP_1:10;
A14: a * (- (/ a)) = - (1. N) by A2, A4, A12, VECTSP_1:8;
thus (- a) *' = ((- a) *') * (1. N) by A5
.= (((- a) *') * (- a)) * (- (/ a)) by A13, A3
.= (a *') * (a * (- (/ a))) by A8, A9, A10, A3
.= - (a *') by A2, A14, A4, A5, VECTSP_2:28 ; :: thesis: verum

end;

suppose a is zero ; :: thesis: (- a) *' = - (a *')

then A15: ( a = 0. N & a *' = 0. N ) by A1;
- (0. N) = 0. N by A2;
hence (- a) *' = - (a *') by A15; :: thesis: verum

end;

end;