let K be Field; :: thesis: for p1, p2 being FinSequence of K holds dom (p1 + p2) = (dom p1) /\ (dom p2)
let p1, p2 be FinSequence of K; :: thesis: dom (p1 + p2) = (dom p1) /\ (dom p2)
( rng p1 c= the carrier of K & rng p2 c= the carrier of K ) by FINSEQ_1:def 4;
then [:(rng p1),(rng p2):] c= [: the carrier of K, the carrier of K:] by ZFMISC_1:96;
then [:(rng p1),(rng p2):] c= dom the addF of K by FUNCT_2:def 1;
hence dom (p1 + p2) = (dom p1) /\ (dom p2) by FUNCOP_1:69; :: thesis: verum