A1: ( INT.Group = multMagma(# INT ,addint #) & dom addint = [:INT ,INT :] & [:INT ,INT :] c= [:REAL ,REAL :] & dom addreal = [:REAL ,REAL :] ) by FUNCT_2:def 1, GR_CY_1:def 4, NUMBERS:15, ZFMISC_1:119;
then A2: dom (addreal || INT ) = [:INT ,INT :] by RELAT_1:91;

now

let x be set ; :: thesis: ( x in [:INT ,INT :] implies addint . x = (addreal || INT ) . x )
assume A3: x in [:INT ,INT :] ; :: thesis: addint . x = (addreal || INT ) . x
then A4: ( x `1 in INT & x `2 in INT & x = [(x `1 ),(x `2 )] ) by MCART_1:10, MCART_1:23;
reconsider i1 = x `1 , i2 = x `2 as Element of INT by A3, MCART_1:10;
thus addint . x = addint . i1,i2 by A3, MCART_1:23
.= addreal . i1,i2 by GR_CY_1:def 2
.= (addreal || INT ) . x by A2, A3, A4, FUNCT_1:70 ; :: thesis: verum

end;

then A5: addint = addreal || INT by A1, A2, FUNCT_1:9;
INT.Group is SubStr of <REAL,+>

proof

thus H₂( INT.Group ) c= H₂( <REAL,+> ) by A5, GR_CY_1:def 4, RELAT_1:88; :: according to MONOID_0:def 23 :: thesis: verum

end;

hence INT.Group is non empty strict unital invertible SubStr of <REAL,+> ; :: thesis: verum