let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; :: thesis: for V being non empty right_complementable VectSp-like Abelian add-associative right_zeroed VectSpStr of GF
for v1, v2, v3 being Element of V
for f being Function of the carrier of V,the carrier of GF holds f (#) <*v1,v2,v3*> = <*((f . v1) * v1),((f . v2) * v2),((f . v3) * v3)*>
let V be non empty right_complementable VectSp-like Abelian add-associative right_zeroed VectSpStr of GF; :: thesis: for v1, v2, v3 being Element of V
for f being Function of the carrier of V,the carrier of GF holds f (#) <*v1,v2,v3*> = <*((f . v1) * v1),((f . v2) * v2),((f . v3) * v3)*>
let v1, v2, v3 be Element of V; :: thesis: for f being Function of the carrier of V,the carrier of GF holds f (#) <*v1,v2,v3*> = <*((f . v1) * v1),((f . v2) * v2),((f . v3) * v3)*>
let f be Function of the carrier of V,the carrier of GF; :: thesis: f (#) <*v1,v2,v3*> = <*((f . v1) * v1),((f . v2) * v2),((f . v3) * 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 = (f . (<*v1,v2,v3*> /. 1)) * (<*v1,v2,v3*> /. 1) by Def8
.= (f . (<*v1,v2,v3*> /. 1)) * v1 by FINSEQ_4:27
.= (f . v1) * v1 by FINSEQ_4:27 ;
A4: (f (#) <*v1,v2,v3*>) . 2 = (f . (<*v1,v2,v3*> /. 2)) * (<*v1,v2,v3*> /. 2) by A2, Def8
.= (f . (<*v1,v2,v3*> /. 2)) * v2 by FINSEQ_4:27
.= (f . v2) * v2 by FINSEQ_4:27 ;
(f (#) <*v1,v2,v3*>) . 3 = (f . (<*v1,v2,v3*> /. 3)) * (<*v1,v2,v3*> /. 3) by A2, Def8
.= (f . (<*v1,v2,v3*> /. 3)) * v3 by FINSEQ_4:27
.= (f . v3) * v3 by FINSEQ_4:27 ;
hence f (#) <*v1,v2,v3*> = <*((f . v1) * v1),((f . v2) * v2),((f . v3) * v3)*> by A1, A3, A4, FINSEQ_1:62; :: thesis: verum