let i be Element of NAT ; :: thesis: for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for v being Element of V

for F being FinSequence of V

for f being Function of V,GF st i in dom F & v = F . i holds

(f (#) F) . i = (f . v) * v

let GF be non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr ; :: thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for v being Element of V

for F being FinSequence of V

for f being Function of V,GF st i in dom F & v = F . i holds

(f (#) F) . i = (f . v) * v

let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF; :: thesis: for v being Element of V

for F being FinSequence of V

for f being Function of V,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 V

for f being Function of V,GF st i in dom F & v = F . i holds

(f (#) F) . i = (f . v) * v

let F be FinSequence of V; :: thesis: for f being Function of V,GF st i in dom F & v = F . i holds

(f (#) F) . i = (f . v) * v

let f be Function of V,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

A3: F /. i = F . i by A1, PARTFUN1:def 6;

len (f (#) F) = len F by Def5;

then i in dom (f (#) F) by A1, FINSEQ_3:29;

hence (f (#) F) . i = (f . v) * v by A2, A3, Def5; :: thesis: verum

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for v being Element of V

for F being FinSequence of V

for f being Function of V,GF st i in dom F & v = F . i holds

(f (#) F) . i = (f . v) * v

let GF be non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr ; :: thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for v being Element of V

for F being FinSequence of V

for f being Function of V,GF st i in dom F & v = F . i holds

(f (#) F) . i = (f . v) * v

let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF; :: thesis: for v being Element of V

for F being FinSequence of V

for f being Function of V,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 V

for f being Function of V,GF st i in dom F & v = F . i holds

(f (#) F) . i = (f . v) * v

let F be FinSequence of V; :: thesis: for f being Function of V,GF st i in dom F & v = F . i holds

(f (#) F) . i = (f . v) * v

let f be Function of V,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

A3: F /. i = F . i by A1, PARTFUN1:def 6;

len (f (#) F) = len F by Def5;

then i in dom (f (#) F) by A1, FINSEQ_3:29;

hence (f (#) F) . i = (f . v) * v by A2, A3, Def5; :: thesis: verum