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
A3: F /. x = F . x by A1, PARTFUN1:def 6;
len (f (#) F) = len F by Def5;
then x in dom (f (#) F) by A1, FINSEQ_3:29;
hence (f (#) F) . x = (f . v) * v by A2, A3, Def5; :: thesis: verum