let K be Field; :: thesis: for V1, V2 being finite-dimensional VectSp of K
for f being Function of V1,V2
for a being FinSequence of K
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 V1, V2 be finite-dimensional VectSp of K; :: thesis: for f being Function of V1,V2
for a being FinSequence of K
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 K
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 K; :: 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 by FINSEQ_1:def 4;
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 ;
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 ;
A11: (f * p) /. k = (f * p) . k by ;
thus (f * (lmlt (a,p))) . k = f . ((lmlt (a,p)) . k) by
.= f . ( the lmult of V1 . ((a . k),(p . k))) by
.= f . ((a /. k) * (p /. k)) by
.= (a /. k) * (f . (p /. k)) by
.= (a /. k) * ((f * p) /. k) by
.= the lmult of V2 . ((a . k),((f * p) . k)) by
.= (lmlt (a,(f * p))) . k by ; :: thesis: verum
end;
dom (lmlt (a,p)) = dom p by
.= 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 ; :: thesis: verum