let N be non empty ConjNormAlgStr ; :: thesis: for a, b 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 & N is add-conjugative holds
(a - b) *' = (a *') - (b *')
let a, b 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 & N is add-conjugative implies (a - b) *' = (a *') - (b *') )
assume A1: ( 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 ) ; :: thesis: ( not N is add-conjugative or (a - b) *' = (a *') - (b *') )
assume N is add-conjugative ; :: thesis: (a - b) *' = (a *') - (b *')
hence (a - b) *' = (a *') + ((- b) *')
.= (a *') - (b *') by A1, Th10 ;
:: thesis: verum