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 Th23;
then reconsider x = a as Real ;

now :: thesis: for b being Element of N holds
( H₂(N) . (a,b) = b & H₂(N) . (b,a) = b )

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: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