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 Def6
.= 3 by FINSEQ_1:45 ;
then A2: dom (f (#) <*v1,v2,v3*>) = {1,2,3} by FINSEQ_1:def 3, FINSEQ_3:1;
3 in {1,2,3} by ENUMSET1:def 1;
then A3: (f (#) <*v1,v2,v3*>) . 3 = (<*v1,v2,v3*> /. 3) * (f . (<*v1,v2,v3*> /. 3)) by A2, Def6
.= v3 * (f . (<*v1,v2,v3*> /. 3)) by FINSEQ_4:18
.= v3 * (f . v3) by FINSEQ_4:18 ;
2 in {1,2,3} by ENUMSET1:def 1;
then A4: (f (#) <*v1,v2,v3*>) . 2 = (<*v1,v2,v3*> /. 2) * (f . (<*v1,v2,v3*> /. 2)) by A2, Def6
.= v2 * (f . (<*v1,v2,v3*> /. 2)) by FINSEQ_4:18
.= v2 * (f . v2) by FINSEQ_4:18 ;
1 in {1,2,3} by ENUMSET1:def 1;
then (f (#) <*v1,v2,v3*>) . 1 = (<*v1,v2,v3*> /. 1) * (f . (<*v1,v2,v3*> /. 1)) by A2, Def6
.= v1 * (f . (<*v1,v2,v3*> /. 1)) by FINSEQ_4:18
.= v1 * (f . v1) by FINSEQ_4:18 ;
hence f (#) <*v1,v2,v3*> = <*(v1 * (f . v1)),(v2 * (f . v2)),(v3 * (f . v3))*> by A1, A4, A3, FINSEQ_1:45; :: thesis: verum