let F be FinSequence of COMPLEX ; :: thesis: for x being Element of COMPLEX holds Sum (F ^ <*x*>) = (Sum F) + x
let x be Element of COMPLEX ; :: thesis: Sum (F ^ <*x*>) = (Sum F) + x
thus Sum (F ^ <*x*>) = addcomplex . ((addcomplex $$ F),x) by FINSOP_1:4
.= (Sum F) + x by BINOP_2:def 3 ; :: thesis: verum