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;
H₁(N) c= REAL by Th25;
then reconsider x = a as Real by TARSKI:def 3;

now

let b be Element of N; :: thesis: ( H₂(N) . a,b = b & H₂(N) . b,a = b )
( a * b = H₂(N) . a,b & b * a = H₂(N) . b,a ) ;
hence ( H₂(N) . a,b = b & H₂(N) . b,a = b ) by A1; :: thesis: verum

end;

then A2: a is_a_unity_wrt H₂(N) by BINOP_1:11;
x + 0 = a * a by A1
.= x + x by Th43 ;
hence the_unity_wrt the multF of N = 0 by A2, BINOP_1:def 8; :: thesis: verum