assume A2:
( a = c & b = d )
; :: thesis: a + b = c + d

addint . (a,b) = addreal . (a,b) by GR_CY_1:def 1

.= c + d by A2, BINOP_2:def 9 ;

hence a + b = c + d ; :: thesis: verum

addint . (a,b) = addreal . (a,b) by GR_CY_1:def 1

.= c + d by A2, BINOP_2:def 9 ;

hence a + b = c + d ; :: thesis: verum