set f = addint || NAT;
dom addint = [:INT,INT:] by FUNCT_2:def 1;
then A1: dom (addint || NAT) = [:NAT,NAT:] by NUMBERS:17, RELAT_1:62, ZFMISC_1:96;
rng (addint || NAT) c= NAT

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (addint || NAT) or x in NAT )
assume x in rng (addint || NAT) ; :: thesis: x in NAT
then consider y being object such that
A2: y in dom (addint || NAT) and
A3: x = (addint || NAT) . y by FUNCT_1:def 3;
reconsider n1 = y `1 , n2 = y `2 as Element of NAT by A1, A2, MCART_1:10;
reconsider i1 = n1, i2 = n2 as Integer ;
x = addint . y by A2, A3, FUNCT_1:47
.= addint . (i1,i2) by A1, A2, MCART_1:21
.= n1 + n2 by BINOP_2:def 20 ;
hence x in NAT by ORDINAL1:def 12; :: thesis: verum

end;

then reconsider f = addint || NAT as BinOp of NAT by A1, FUNCT_2:def 1, RELSET_1:4;
f c= H₂( INT.Group ) by GR_CY_1:def 3, RELAT_1:59;
then reconsider N = multMagma(# NAT,f #) as non empty strict SubStr of INT.Group by Def23;
reconsider a = 0 as Element of N ;

A4: 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 = 0 + n by Th39
.= b ; :: thesis: b * a = b
thus b * a = n + 0 by Th39
.= 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 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:3;
then A6: the_unity_wrt H₂(N) = a by BINOP_1:def 8;

A7: 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 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 Th39;
then a = 0 by A6, A8;
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;
then N is uniquely-decomposable by A7, Th14;
hence ex b₁ being non empty strict unital uniquely-decomposable SubStr of INT.Group st the carrier of b₁ = NAT by A10; :: thesis: verum