let d, e be XFinSequence of ; :: thesis: Sum (d ^ e) = (Sum d) + (Sum e)
thus Sum (d ^ e) = addnat . (Sum d),(Sum e) by STIRL2_1:47
.= (Sum d) + (Sum e) by BINOP_2:def 23 ; :: thesis: verum