set f = multreal || NAT;
A1: dom multreal = [:REAL,REAL:] by FUNCT_2:def 1;
[:NAT,NAT:] c= [:REAL,REAL:] by ZFMISC_1:96, NUMBERS:19;
then A2: dom (multreal || NAT) = [:NAT,NAT:] by RELAT_1:62, A1;
rng (multreal || NAT) c= NAT

proof

let x be object ; :: 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 object such that
A3: y in dom (multreal || NAT) and
A4: x = (multreal || NAT) . y by FUNCT_1:def 3;
reconsider n1 = y `1 , n2 = y `2 as Element of NAT by A2, A3, MCART_1:10;
x = multreal . y by A3, A4, FUNCT_1:47
.= multreal . (n1,n2) by A2, A3, MCART_1:21
.= n1 * n2 by BINOP_2:def 11 ;
hence x in NAT by ORDINAL1:def 12; :: thesis: verum

end;

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

A5: now :: thesis: for b being Element of N holds
( a * b = b & b * a = b )

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 Th50
.= b ; :: thesis: b * a = b
thus b * a = n * 1 by Th50
.= b ; :: thesis: verum

end;

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 )
thus H₂(N) . (a,b) = a * b
.= b by A5 ; :: thesis: H₂(N) . (b,a) = b
thus H₂(N) . (b,a) = b * a
.= b by A5 ; :: thesis: verum

end;

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

A8: now :: thesis: for a, b being Element of N st a * b = the_unity_wrt H₂(N) holds
( a = b & b = the_unity_wrt H₂(N) )

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 A9: 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 ;
A10: a * b = n * m by Th50;
then a = 1 by A7, A9, NAT_1:15;
hence ( a = b & b = the_unity_wrt H₂(N) ) by A6, A9, A10, BINOP_1:def 8; :: thesis: verum

end;

A11: N is unital by A5;
then N is uniquely-decomposable by A8, Th14;
hence ex b₁ being non empty strict unital uniquely-decomposable SubStr of <REAL,*> st the carrier of b₁ = NAT by A11; :: thesis: verum