let V be non empty CLSStruct ; :: thesis: for v being VECTOR of V
for x being set
for F being FinSequence of the carrier of V
for f being Function of the carrier of V,COMPLEX st x in dom F & v = F . x holds
(f (#) F) . x = (f . v) * v
let v be VECTOR of V; :: thesis: for x being set
for F being FinSequence of the carrier of V
for f being Function of the carrier of V,COMPLEX st x in dom F & v = F . x holds
(f (#) F) . x = (f . v) * v
let x be set ; :: thesis: for F being FinSequence of the carrier of V
for f being Function of the carrier of V,COMPLEX st x in dom F & v = F . x holds
(f (#) F) . x = (f . v) * v
let F be FinSequence of the carrier of V; :: thesis: for f being Function of the carrier of V,COMPLEX st x in dom F & v = F . x holds
(f (#) F) . x = (f . v) * v
let f be Function of the carrier of V,COMPLEX ; :: thesis: ( x in dom F & v = F . x implies (f (#) F) . x = (f . v) * v )
assume that
A1: x in dom F and
A2: v = F . x ; :: thesis: (f (#) F) . x = (f . v) * v
len (f (#) F) = len F by Def4;
then A3: x in dom (f (#) F) by A1, FINSEQ_3:31;
A4: F /. x = F . x by A1, PARTFUN1:def 8;
reconsider i = x as Nat by A1;
(f (#) F) . i = (f . v) * v by A2, A3, A4, Def4;
hence (f (#) F) . x = (f . v) * v ; :: thesis: verum