assume A3: ( a = c & b = d ) ; :: thesis: a + b = c + d
reconsider a = a, b = b as Element of INT ;
A4: ( a is Element of REAL & b is Element of REAL ) by XREAL_0:def 1;
addint . a,b = addreal . a,b by GR_CY_1:def 2
.= c + d by A3, A4, BINOP_2:def 9 ;
hence a + b = c + d ; :: thesis: verum