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