let V1, V2 be free finite-rank Z_Module; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( len p = len a & f is additive & f is homogeneous implies f * (lmlt (a,p)) = lmlt (a,(f * p)) )
assume len p = len a ; :: thesis: ( 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 ) ; :: thesis: f * (lmlt (a,p)) = lmlt (a,(f * p))

A4: now :: thesis: for k being Nat st k in dom (f * (lmlt (a,p))) holds
(f * (lmlt (a,p))) . k = (lmlt (a,(f * p))) . k

set P = f * p;
let k be Nat; :: thesis: ( 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))) ; :: thesis: (f * (lmlt (a,p))) . k = (lmlt (a,(f * p))) . k
A6: 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 ; :: thesis: 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; :: thesis: verum