dom addreal = [:REAL ,REAL :] by FUNCT_2:def 1;
then A1: dom (addreal || INT ) = [:INT ,INT :] by NUMBERS:15, RELAT_1:91, ZFMISC_1:119;

A2: 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 = [(x `1 ),(x `2 )] by 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 A1, A3, A4, FUNCT_1:70 ; :: thesis: verum

end;

dom addint = [:INT ,INT :] by FUNCT_2:def 1;
then addint = addreal || INT by A1, A2, FUNCT_1:9;
then H₂( INT.Group ) c= H₂( <REAL,+> ) by GR_CY_1:def 4, RELAT_1:88;
hence INT.Group is non empty strict unital invertible SubStr of <REAL,+> by Def23; :: thesis: verum