let N be non empty unital SubStr of <REAL,*> ; :: thesis: ( the_unity_wrt the multF of N = 0 or the_unity_wrt the multF of N = 1 )
set e = the_unity_wrt H₂(N);
H₁(N) c= H₁( <REAL,*> ) by Th23;
then reconsider x = the_unity_wrt H₂(N) as Real ;
the_unity_wrt H₂(N) is_a_unity_wrt H₂(N) by Th4;
then the_unity_wrt H₂(N) = (the_unity_wrt H₂(N)) * (the_unity_wrt H₂(N)) by BINOP_1:3
.= x * x by Th50 ;
then x * 1 = x * x ;
hence ( the_unity_wrt the multF of N = 0 or the_unity_wrt the multF of N = 1 ) by XCMPLX_1:5; :: thesis: verum