let K be Field; 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; 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; ( 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
; (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 for x being object st x in dom f holds
((p + q) * f) . x = (pf9 + qf9) . xA13:
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 ;
( x in dom f implies ((p + q) * f) . x = (pf9 + qf9) . x )assume A15:
x in dom f
;
((p + q) * f) . x = (pf9 + qf9) . xA16:
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
;
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; verum