let R be Ring; :: thesis: for V being RightMod of R
for i being Nat
for v being Vector of V
for F being FinSequence of V
for f being Function of V,R st i in dom F & v = F . i holds
(f (#) F) . i = v * (f . v)
let V be RightMod of R; :: thesis: for i being Nat
for v being Vector of V
for F being FinSequence of V
for f being Function of V,R st i in dom F & v = F . i holds
(f (#) F) . i = v * (f . v)
let i be Nat; :: thesis: for v being Vector of V
for F being FinSequence of V
for f being Function of V,R st i in dom F & v = F . i holds
(f (#) F) . i = v * (f . v)
let v be Vector of V; :: thesis: for F being FinSequence of V
for f being Function of V,R st i in dom F & v = F . i holds
(f (#) F) . i = v * (f . v)
let F be FinSequence of V; :: thesis: for f being Function of V,R st i in dom F & v = F . i holds
(f (#) F) . i = v * (f . v)
let f be Function of V,R; :: thesis: ( i in dom F & v = F . i implies (f (#) F) . i = v * (f . v) )
assume that
A1: i in dom F and
A2: v = F . i ; :: thesis: (f (#) F) . i = v * (f . v)
A3: F /. i = F . i by A1, PARTFUN1:def 6;
len (f (#) F) = len F by Def6;
then i in dom (f (#) F) by A1, FINSEQ_3:29;
hence (f (#) F) . i = v * (f . v) by A2, A3, Def6; :: thesis: verum