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

proof

let x be set ; :: 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 set such that
A2: ( y in dom (addint || NAT ) & x = (addint || NAT ) . y ) by FUNCT_1:def 5;
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, FUNCT_1:70
.= addint . i1,i2 by A1, A2, MCART_1:23
.= n1 + n2 by GR_CY_1:14 ;
hence x in NAT ; :: thesis: verum

end;

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

A3: now

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

end;

then A4: N is unital by Th6;
then A5: H₂(N) is having_a_unity by Def10;

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

end;

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

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 ;
a * b = n + m by Th43;
then ( a = 0 & b = 0 ) by A7, A8, NAT_1:7;
hence ( a = b & b = the_unity_wrt H₂(N) ) by A6, BINOP_1:def 8; :: thesis: verum

end;

then N is uniquely-decomposable by A5, Th16;
hence ex b₁ being non empty strict unital uniquely-decomposable SubStr of INT.Group st the carrier of b₁ = NAT by A4; :: thesis: verum