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))

.= 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

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

dom (lmlt (a,p)) =
dom p
by A1, Th12
(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 . ( the lmult of V1 . ((a . k),(p . k))) by A5, A6, FUNCOP_1:22

.= f . ((a /. k) * (p /. k)) by A10, A8, VECTSP_1:def 12

.= (a /. k) * (f . (p /. k)) by A3, MOD_2:def 2

.= (a /. k) * ((f * p) /. k) by A7, A8, A11, FUNCT_1:13

.= the lmult of V2 . ((a . k),((f * p) . k)) by A10, A11, VECTSP_1:def 12

.= (lmlt (a,(f * p))) . k by A9, FUNCOP_1:22 ; :: thesis: verum

end;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 . ( the lmult of V1 . ((a . k),(p . k))) by A5, A6, FUNCOP_1:22

.= f . ((a /. k) * (p /. k)) by A10, A8, VECTSP_1:def 12

.= (a /. k) * (f . (p /. k)) by A3, MOD_2:def 2

.= (a /. k) * ((f * p) /. k) by A7, A8, A11, FUNCT_1:13

.= the lmult of V2 . ((a . k),((f * p) . k)) by A10, A11, VECTSP_1:def 12

.= (lmlt (a,(f * p))) . k by A9, FUNCOP_1:22 ; :: thesis: verum

.= 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