let N be non empty unital SubStr of <REAL,+> ; :: thesis: the_unity_wrt the multF of N = 0
consider a being Element of N such that
A1: for b being Element of N holds
( a * b = b & b * a = b ) by Th6;
H1(N) c= REAL by Th23;
then reconsider x = a as Real ;
now :: thesis: for b being Element of N holds
( H2(N) . (a,b) = b & H2(N) . (b,a) = b )
let b be Element of N; :: thesis: ( H2(N) . (a,b) = b & H2(N) . (b,a) = b )
( a * b = H2(N) . (a,b) & b * a = H2(N) . (b,a) ) ;
hence ( H2(N) . (a,b) = b & H2(N) . (b,a) = b ) by A1; :: thesis: verum
end;
then A2: a is_a_unity_wrt H2(N) by BINOP_1:3;
x + 0 = a * a by A1
.= x + x by Th39 ;
hence the_unity_wrt the multF of N = 0 by A2, BINOP_1:def 8; :: thesis: verum