let R be Ring; :: thesis: for V being RightMod of R
for v being Vector of V
for f being Function of V,R holds f (#) <*v*> = <*(v * (f . v))*>
let V be RightMod of R; :: thesis: for v being Vector of V
for f being Function of V,R holds f (#) <*v*> = <*(v * (f . v))*>
let v be Vector of V; :: thesis: for f being Function of V,R holds f (#) <*v*> = <*(v * (f . v))*>
let f be Function of V,R; :: thesis: f (#) <*v*> = <*(v * (f . v))*>
A1: 1 in {1} by TARSKI:def 1;
A2: len (f (#) <*v*>) = len <*v*> by Def6
.= 1 by FINSEQ_1:40 ;
then dom (f (#) <*v*>) = {1} by FINSEQ_1:2, FINSEQ_1:def 3;
then (f (#) <*v*>) . 1 = (<*v*> /. 1) * (f . (<*v*> /. 1)) by A1, Def6
.= v * (f . (<*v*> /. 1)) by FINSEQ_4:16
.= v * (f . v) by FINSEQ_4:16 ;
hence f (#) <*v*> = <*(v * (f . v))*> by A2, FINSEQ_1:40; :: thesis: verum