let p, q be XFinSequence of NAT ; :: thesis: Sum (p ^ q) = (Sum p) + (Sum q)
addnat "**" (p ^ q) = addnat . (addnat "**" p),(addnat "**" q) by STIRL2_1:47;
hence Sum (p ^ q) = (Sum p) + (Sum q) by BINOP_2:def 23; :: thesis: verum