let p, q be FinSequence of INT ; :: thesis: Sum (p ^ q) = (Sum p) + (Sum q)
A1: rng p c= REAL by NUMBERS:15, XBOOLE_1:1;
rng q c= REAL by NUMBERS:15, XBOOLE_1:1;
then reconsider p = p, q = q as real-valued FinSequence by A1, VALUED_0:def 3;
Sum (p ^ q) = (Sum p) + (Sum q) by RVSUM_1:105;
hence Sum (p ^ q) = (Sum p) + (Sum q) ; :: thesis: verum