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