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