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