let i be Element of NAT ; :: thesis: for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable VectSp-like Abelian add-associative right_zeroed VectSpStr of GF
for v being Element of V
for F being FinSequence of the carrier of V
for f being Function of the carrier of V,the carrier of GF st i in dom F & v = F . i holds
(f (#) F) . i = (f . v) * v
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 v being Element of V
for F being FinSequence of the carrier of V
for f being Function of the carrier of V,the carrier of GF st i in dom F & v = F . i holds
(f (#) F) . i = (f . v) * v
let V be non empty right_complementable VectSp-like Abelian add-associative right_zeroed VectSpStr of GF; :: thesis: for v being Element of V
for F being FinSequence of the carrier of V
for f being Function of the carrier of V,the carrier of GF st i in dom F & v = F . i holds
(f (#) F) . i = (f . v) * v
let v be Element of V; :: thesis: for F being FinSequence of the carrier of V
for f being Function of the carrier of V,the carrier of GF st i in dom F & v = F . i holds
(f (#) F) . i = (f . v) * v
let F be FinSequence of the carrier of V; :: thesis: for f being Function of the carrier of V,the carrier of GF st i in dom F & v = F . i holds
(f (#) F) . i = (f . v) * v
let f be Function of the carrier of V,the carrier of GF; :: thesis: ( i in dom F & v = F . i implies (f (#) F) . i = (f . v) * v )
assume that
A1: i in dom F and
A2: v = F . i ; :: thesis: (f (#) F) . i = (f . v) * v
len (f (#) F) = len F by Def8;
then A3: i in dom (f (#) F) by A1, FINSEQ_3:31;
F /. i = F . i by A1, PARTFUN1:def 8;
hence (f (#) F) . i = (f . v) * v by A2, A3, Def8; :: thesis: verum