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

A2: now :: thesis: for x being object st x in [:INT,INT:] holds
addint . x = (addreal || INT) . x

let x be object ; :: 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:21;
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:21
.= addreal . (i1,i2) by GR_CY_1:def 1
.= (addreal || INT) . x by A1, A3, A4, FUNCT_1:47 ; :: thesis: verum

end;

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