let K be Field; :: thesis: for p, pf, q, qf being FinSequence of K
for f being Function st pf = p * f & rng f c= dom p & qf = q * f & rng f c= dom q holds
(p + q) * f = pf + qf
let p, pf, q, qf be FinSequence of K; :: thesis: for f being Function st pf = p * f & rng f c= dom p & qf = q * f & rng f c= dom q holds
(p + q) * f = pf + qf
let f be Function; :: thesis: ( pf = p * f & rng f c= dom p & qf = q * f & rng f c= dom q implies (p + q) * f = pf + qf )
assume that
A1: pf = p * f and
A2: rng f c= dom p and
A3: qf = q * f and
A4: rng f c= dom q ; :: thesis: (p + q) * f = pf + qf
A5: dom pf = dom f by A1, A2, RELAT_1:27;
set KK = the carrier of K;
A6: dom pf = Seg (len pf) by FINSEQ_1:def 3;
A7: dom qf = dom f by A3, A4, RELAT_1:27;
then len qf = len pf by A5, A6, FINSEQ_1:def 3;
then reconsider pf9 = pf, qf9 = qf as Element of (len pf) -tuples_on the carrier of K by FINSEQ_2:92;
A8: dom (pf9 + qf9) = dom f by A5, A6, FINSEQ_2:124;
set pq = p + q;
A9: rng q c= the carrier of K by FINSEQ_1:def 4;
rng p c= the carrier of K by FINSEQ_1:def 4;
then [:(rng p),(rng q):] c= [: the carrier of K, the carrier of K:] by A9, ZFMISC_1:96;
then [:(rng p),(rng q):] c= dom the addF of K by FUNCT_2:def 1;
then A10: dom (p + q) = (dom p) /\ (dom q) by FUNCOP_1:69;
then A11: rng f c= dom (p + q) by A2, A4, XBOOLE_1:19;

A12: now :: thesis: for x being object st x in dom f holds
((p + q) * f) . x = (pf9 + qf9) . x

A13: rng qf c= the carrier of K by FINSEQ_1:def 4;
A14: rng pf c= the carrier of K by FINSEQ_1:def 4;
let x be object ; :: thesis: ( x in dom f implies ((p + q) * f) . x = (pf9 + qf9) . x )
assume A15: x in dom f ; :: thesis: ((p + q) * f) . x = (pf9 + qf9) . x
A16: f . x in rng f by A15, FUNCT_1:def 3;
dom p = Seg (len p) by FINSEQ_1:def 3;
then f . x in Seg (len p) by A2, A16;
then reconsider n = x, fx = f . x as Element of NAT by A5, A15;
A17: qf . x in rng qf by A7, A15, FUNCT_1:def 3;
pf . x in rng pf by A5, A15, FUNCT_1:def 3;
then reconsider pfn = pf . n, qfn = qf . n as Element of K by A14, A17, A13;
A18: pfn = p . fx by A1, A15, FUNCT_1:13;
A19: qfn = q . fx by A3, A15, FUNCT_1:13;
thus ((p + q) * f) . x = (p + q) . fx by A15, FUNCT_1:13
.= pfn + qfn by A11, A16, A18, A19, FVSUM_1:17
.= (pf9 + qf9) . x by A5, A6, A15, FVSUM_1:18 ; :: thesis: verum

end;

dom ((p + q) * f) = dom f by A2, A4, A10, RELAT_1:27, XBOOLE_1:19;
hence (p + q) * f = pf + qf by A8, A12; :: thesis: verum