let R be Ring; :: thesis: for V being RightMod of R
for v1, v2, v3 being Vector of V
for f being Function of V,R holds f (#) <*v1,v2,v3*> = <*(v1 * (f . v1)),(v2 * (f . v2)),(v3 * (f . v3))*>
let V be RightMod of R; :: thesis: for v1, v2, v3 being Vector of V
for f being Function of V,R holds f (#) <*v1,v2,v3*> = <*(v1 * (f . v1)),(v2 * (f . v2)),(v3 * (f . v3))*>
let v1, v2, v3 be Vector of V; :: thesis: for f being Function of V,R holds f (#) <*v1,v2,v3*> = <*(v1 * (f . v1)),(v2 * (f . v2)),(v3 * (f . v3))*>
let f be Function of V,R; :: thesis: f (#) <*v1,v2,v3*> = <*(v1 * (f . v1)),(v2 * (f . v2)),(v3 * (f . v3))*>
A1: len (f (#) <*v1,v2,v3*>) = len <*v1,v2,v3*> by Def8
.= 3 by FINSEQ_1:62 ;
then A2: ( dom (f (#) <*v1,v2,v3*>) = {1,2,3} & 1 in {1,2,3} & 2 in {1,2,3} & 3 in {1,2,3} ) by ENUMSET1:def 1, FINSEQ_1:def 3, FINSEQ_3:1;
then A3: (f (#) <*v1,v2,v3*>) . 1 = (<*v1,v2,v3*> /. 1) * (f . (<*v1,v2,v3*> /. 1)) by Def8
.= v1 * (f . (<*v1,v2,v3*> /. 1)) by FINSEQ_4:27
.= v1 * (f . v1) by FINSEQ_4:27 ;
A4: (f (#) <*v1,v2,v3*>) . 2 = (<*v1,v2,v3*> /. 2) * (f . (<*v1,v2,v3*> /. 2)) by A2, Def8
.= v2 * (f . (<*v1,v2,v3*> /. 2)) by FINSEQ_4:27
.= v2 * (f . v2) by FINSEQ_4:27 ;
(f (#) <*v1,v2,v3*>) . 3 = (<*v1,v2,v3*> /. 3) * (f . (<*v1,v2,v3*> /. 3)) by A2, Def8
.= v3 * (f . (<*v1,v2,v3*> /. 3)) by FINSEQ_4:27
.= v3 * (f . v3) by FINSEQ_4:27 ;
hence f (#) <*v1,v2,v3*> = <*(v1 * (f . v1)),(v2 * (f . v2)),(v3 * (f . v3))*> by A1, A3, A4, FINSEQ_1:62; :: thesis: verum