let K be Field; :: thesis: for V2, V1 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 linear holds
f * (lmlt a,p) = lmlt a,(f * p)
let V2, V1 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 linear 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 linear 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 linear holds
f * (lmlt a,p) = lmlt a,(f * p)
let p be FinSequence of V1; :: thesis: ( len p = len a & f is linear implies f * (lmlt a,p) = lmlt a,(f * p) )
assume len p = len a ; :: thesis: ( not f is linear or f * (lmlt a,p) = lmlt a,(f * p) )
then A1: dom p = dom a by FINSEQ_3:31;
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:46;
assume A3: f is linear ; :: thesis: f * (lmlt a,p) = lmlt a,(f * p)

A4: now

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:44;
then k in dom (lmlt a,p) by A5;
then A7: k in dom p by A1, Th16;
then A8: p /. k = p . k by PARTFUN1:def 8;
A9: k in dom (lmlt a,(f * p)) by A1, A2, A7, Th16;
A10: a /. k = a . k by A1, A7, PARTFUN1:def 8;
A11: (f * p) /. k = (f * p) . k by A2, A7, PARTFUN1:def 8;
thus (f * (lmlt a,p)) . k = f . ((lmlt a,p) . k) by A5, FUNCT_1:22
.= f . (the lmult of V1 . (a . k),(p . k)) by A5, A6, FUNCOP_1:28
.= f . ((a /. k) * (p /. k)) by A10, A8, VECTSP_1:def 24
.= (a /. k) * (f . (p /. k)) by A3, MOD_2:def 5
.= (a /. k) * ((f * p) /. k) by A7, A8, A11, FUNCT_1:23
.= the lmult of V2 . (a . k),((f * p) . k) by A10, A11, VECTSP_1:def 24
.= (lmlt a,(f * p)) . k by A9, FUNCOP_1:28 ; :: thesis: verum

end;

dom (lmlt a,p) = dom p by A1, Th16
.= dom (lmlt a,(f * p)) by A1, A2, Th16 ;
then len (lmlt a,p) = len (lmlt a,(f * p)) by FINSEQ_3:31;
then len (f * (lmlt a,p)) = len (lmlt a,(f * p)) by FINSEQ_2:37;
hence f * (lmlt a,p) = lmlt a,(f * p) by A4, FINSEQ_2:10; :: thesis: verum