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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (multreal || NAT ) or x in NAT )
assume x in rng (multreal || NAT ) ; :: thesis: x in NAT
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: verum

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: ( a * b = b & b * a = b )
reconsider n = b as Element of NAT ;
thus a * b = 1 * n by Th58
.= b ; :: thesis: b * a = b
thus b * a = n * 1 by Th58
.= b ; :: thesis: verum

end;

now

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

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: ( a * b = the_unity_wrt H₂(N) implies ( a = b & b = the_unity_wrt H₂(N) ) )
assume A8: a * b = the_unity_wrt H₂(N) ; :: thesis: ( a = b & b = the_unity_wrt H₂(N) )
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: verum

end;

A10: N is unital by A4, Th6;
then H₂(N) is having_a_unity by Def10;
then N is uniquely-decomposable by A7, Th16;
hence ex b₁ being non empty strict unital uniquely-decomposable SubStr of <REAL,*> st the carrier of b₁ = NAT by A10; :: thesis: verum