let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in rng (addint || NAT) ; :: thesis:
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:

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 ;

let b be Element of N; :: thesis:
reconsider n = b as Element of NAT ;
thus a * b = 0 + n by Th39
.= b ; :: thesis:
thus b * a = n + 0 by Th39
.= b ; :: thesis:

end;

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;

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 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:

end;