set f = multreal || NAT ;
dom multreal = [:REAL ,REAL :] by FUNCT_2:def 1;
then A1: dom (multreal || NAT ) = [:NAT ,NAT :] by RELAT_1:91;
rng (multreal || NAT ) c= NAT

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in rng (multreal || NAT ) ; :: thesis:
then consider y being set such that
A2: y in dom (multreal || NAT ) and
A3: x = (multreal || NAT ) . y by FUNCT_1:def 5;
reconsider n1 = y `1 , n2 = y `2 as Element of NAT by A1, A2, MCART_1:10;
x = multreal . y by A2, A3, FUNCT_1:70
.= multreal . n1,n2 by A1, A2, MCART_1:23
.= n1 * n2 by BINOP_2:def 11 ;
hence x in NAT ; :: thesis:

end;

then reconsider f = multreal || NAT as BinOp of NAT by A1, FUNCT_2:def 1, RELSET_1:11;
f c= H₂( <REAL,*> ) by RELAT_1:88;
then reconsider N = multMagma(# NAT ,f #) as non empty strict SubStr of <REAL,*> by Def23;
reconsider a = 1 as Element of N ;

A4: now

let b be Element of N; :: thesis:
reconsider n = b as Element of NAT ;
thus a * b = 1 * n by Th58
.= b ; :: thesis:
thus b * a = n * 1 by Th58
.= b ; :: thesis:

end;

now

let b be Element of N; :: thesis:
thus H₂(N) . a,b = a * b
.= b by A4 ; :: thesis:
thus H₂(N) . b,a = b * a
.= b by A4 ; :: thesis:

end;

then A5: a is_a_unity_wrt H₂(N) by BINOP_1:11;
then A6: the_unity_wrt H₂(N) = a by BINOP_1:def 8;

A7: now

let a, b be Element of N; :: thesis:
assume A8: a * b = the_unity_wrt H₂(N) ; :: thesis:
reconsider n = a, m = b as Element of NAT ;
A9: a * b = n * m by Th58;
then a = 1 by A6, A8, NAT_1:15;
hence ( a = b & b = the_unity_wrt H₂(N) ) by A5, A8, A9, BINOP_1:def 8; :: thesis:

end;