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 A1: len p = len a ; :: thesis: ( not f is linear or f * (lmlt a,p) = lmlt a,(f * p) )
assume A2: f is linear ; :: thesis: f * (lmlt a,p) = lmlt a,(f * p)
A3: dom p = dom a by A1, 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 A4: dom p = dom (f * p) by RELAT_1:46;
dom (lmlt a,p) = dom p by A3, Th16
.= dom (lmlt a,(f * p)) by A3, A4, Th16 ;
then len (lmlt a,p) = len (lmlt a,(f * p)) by FINSEQ_3:31;
then A5: len (f * (lmlt a,p)) = len (lmlt a,(f * p)) by FINSEQ_2:37;

now

let k be Nat; :: thesis: ( k in dom (f * (lmlt a,p)) implies (f * (lmlt a,p)) . k = (lmlt a,(f * p)) . k )
assume k in dom (f * (lmlt a,p)) ; :: thesis: (f * (lmlt a,p)) . k = (lmlt a,(f * p)) . k
then A6: k in dom (f * (lmlt a,p)) ;
A7: dom (f * (lmlt a,p)) c= dom (lmlt a,p) by RELAT_1:44;
then k in dom (lmlt a,p) by A6;
then A8: k in dom p by A3, Th16;
then A9: a /. k = a . k by A3, PARTFUN1:def 8;
A10: p /. k = p . k by A8, PARTFUN1:def 8;
set P = f * p;
A11: (f * p) /. k = (f * p) . k by A4, A8, PARTFUN1:def 8;
A12: k in dom (lmlt a,(f * p)) by A3, A4, A8, Th16;
thus (f * (lmlt a,p)) . k = f . ((lmlt a,p) . k) by A6, FUNCT_1:22
.= f . (the lmult of V1 . (a . k),(p . k)) by A6, A7, FUNCOP_1:28
.= f . ((a /. k) * (p /. k)) by A9, A10, VECTSP_1:def 24
.= (a /. k) * (f . (p /. k)) by A2, MOD_2:def 5
.= (a /. k) * ((f * p) /. k) by A8, A10, A11, FUNCT_1:23
.= the lmult of V2 . (a . k),((f * p) . k) by A9, A11, VECTSP_1:def 24
.= (lmlt a,(f * p)) . k by A12, FUNCOP_1:28 ; :: thesis: verum

end;

hence f * (lmlt a,p) = lmlt a,(f * p) by A5, FINSEQ_2:10; :: thesis: verum