let x be Element of REAL ; :: according to FINSEQOP:def 1 :: thesis: ( addreal . x,(compreal . x) = the_unity_wrt addreal & addreal . (compreal . x),x = the_unity_wrt addreal )
thus addreal . x,(compreal . x) = x + (compreal . x) by BINOP_2:def 9
.= x + (- x) by BINOP_2:def 7
.= the_unity_wrt addreal by BINOP_2:2 ; :: thesis: addreal . (compreal . x),x = the_unity_wrt addreal
thus addreal . (compreal . x),x = (compreal . x) + x by BINOP_2:def 9
.= (- x) + x by BINOP_2:def 7
.= the_unity_wrt addreal by BINOP_2:2 ; :: thesis: verum