let c be Element of COMPLEX ; :: according to FINSEQOP:def 1 :: thesis: ( addcomplex . (c,(compcomplex . c)) = the_unity_wrt addcomplex & addcomplex . ((compcomplex . c),c) = the_unity_wrt addcomplex )
thus addcomplex . (c,(compcomplex . c)) = c + (compcomplex . c) by BINOP_2:def 3
.= c + (- c) by BINOP_2:def 1
.= the_unity_wrt addcomplex by BINOP_2:1 ; :: thesis: addcomplex . ((compcomplex . c),c) = the_unity_wrt addcomplex
thus addcomplex . ((compcomplex . c),c) = (compcomplex . c) + c by BINOP_2:def 3
.= (- c) + c by BINOP_2:def 1
.= the_unity_wrt addcomplex by BINOP_2:1 ; :: thesis: verum