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 for x being object st x in [:INT,INT:] holds
addint . x = (addreal || INT) . xlet x be
object ;
( x in [:INT,INT:] implies addint . x = (addreal || INT) . x )assume A3:
x in [:INT,INT:]
;
addint . x = (addreal || INT) . xthen 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
;
verum end;
dom addint = [:INT,INT:]
by FUNCT_2:def 1;
then
addint = addreal || INT
by A1, A2, FUNCT_1:2;
then
H2( INT.Group ) c= H2( <REAL,+> )
by GR_CY_1:def 3, RELAT_1:59;
hence
INT.Group is non empty strict SubStr of <REAL,+>
by Def23; verum