let N be non empty ConjNormAlgStr ; :: thesis: ( ( N is left_unital or N is right_unital ) & N is Banach_Algebra-like_2 & N is almost_right_cancelable & N is well-conjugated & N is scalar-unital implies (1. N) *' = 1. N )
assume that
A1: ( N is left_unital or N is right_unital ) and
A2: N is Banach_Algebra-like_2 and
A3: N is almost_right_cancelable and
A4: N is well-conjugated and
A5: N is scalar-unital ; :: thesis: (1. N) *' = 1. N
per cases ( not 1. N is zero or 1. N is zero ) ;
suppose A6: not 1. N is zero ; :: thesis: (1. N) *' = 1. N
then A7: 1. N <> 0. N ;
A8: ||.(1. N).|| = 1 by A2;
((1. N) *') * (1. N) = (||.(1. N).|| ^2) * (1. N) by A4, A6, Def3
.= 1. N by A8, A5
.= (1. N) * (1. N) by A1 ;
hence (1. N) *' = 1. N by A3, A7, ALGSTR_0:def 21; :: thesis: verum
end;
suppose 1. N is zero ; :: thesis: (1. N) *' = 1. N
then 1. N = (0. N) *' by A4;
hence (1. N) *' = 1. N by A4; :: thesis: verum
end;
end;