let V1, V2 be free finite-rank Z_Module; for f being Function of V1,V2
for a being FinSequence of INT.Ring
for p being FinSequence of V1 st len p = len a & f is additive & f is homogeneous holds
f * (lmlt (a,p)) = lmlt (a,(f * p))
let f be Function of V1,V2; for a being FinSequence of INT.Ring
for p being FinSequence of V1 st len p = len a & f is additive & f is homogeneous holds
f * (lmlt (a,p)) = lmlt (a,(f * p))
let a be FinSequence of INT.Ring; for p being FinSequence of V1 st len p = len a & f is additive & f is homogeneous holds
f * (lmlt (a,p)) = lmlt (a,(f * p))
let p be FinSequence of V1; ( len p = len a & f is additive & f is homogeneous implies f * (lmlt (a,p)) = lmlt (a,(f * p)) )
assume
len p = len a
; ( not f is additive or not f is homogeneous or f * (lmlt (a,p)) = lmlt (a,(f * p)) )
then A1:
dom p = dom a
by FINSEQ_3:29;
dom f = the carrier of V1
by FUNCT_2:def 1;
then
rng p c= dom f
;
then A2:
dom p = dom (f * p)
by RELAT_1:27;
assume A3:
( f is additive & f is homogeneous )
; f * (lmlt (a,p)) = lmlt (a,(f * p))
A4:
now for k being Nat st k in dom (f * (lmlt (a,p))) holds
(f * (lmlt (a,p))) . k = (lmlt (a,(f * p))) . kset P =
f * p;
let k be
Nat;
( k in dom (f * (lmlt (a,p))) implies (f * (lmlt (a,p))) . k = (lmlt (a,(f * p))) . k )assume A5:
k in dom (f * (lmlt (a,p)))
;
(f * (lmlt (a,p))) . k = (lmlt (a,(f * p))) . kA6:
dom (f * (lmlt (a,p))) c= dom (lmlt (a,p))
by RELAT_1:25;
then
k in dom (lmlt (a,p))
by A5;
then A7:
k in dom p
by A1, Th12;
then A8:
p /. k = p . k
by PARTFUN1:def 6;
A9:
k in dom (lmlt (a,(f * p)))
by A1, A2, A7, Th12;
A10:
a /. k = a . k
by A1, A7, PARTFUN1:def 6;
A11:
(f * p) /. k = (f * p) . k
by A2, A7, PARTFUN1:def 6;
thus (f * (lmlt (a,p))) . k =
f . ((lmlt (a,p)) . k)
by A5, FUNCT_1:12
.=
f . ((a /. k) * (p /. k))
by A10, A8, A5, A6, FUNCOP_1:22
.=
(a /. k) * (f . (p /. k))
by A3
.=
(a /. k) * ((f * p) /. k)
by A7, A8, A11, FUNCT_1:13
.=
(lmlt (a,(f * p))) . k
by A9, A10, A11, FUNCOP_1:22
;
verum end;
dom (lmlt (a,p)) =
dom p
by A1, Th12
.=
dom (lmlt (a,(f * p)))
by A1, A2, Th12
;
then
len (lmlt (a,p)) = len (lmlt (a,(f * p)))
by FINSEQ_3:29;
then
len (f * (lmlt (a,p))) = len (lmlt (a,(f * p)))
by FINSEQ_2:33;
hence
f * (lmlt (a,p)) = lmlt (a,(f * p))
by A4, FINSEQ_2:9; verum