let L be Z_Lattice; :: thesis: for f being Function of (DivisibleMod L),INT.Ring

for F being FinSequence of (DivisibleMod L)

for v, u being Vector of (DivisibleMod L)

for i being Nat st i in dom F & u = F . i holds

(ScFS (v,f,F)) . i = (ScProductDM L) . (v,((f . u) * u))

let f be Function of (DivisibleMod L),INT.Ring; :: thesis: for F being FinSequence of (DivisibleMod L)

for v, u being Vector of (DivisibleMod L)

for i being Nat st i in dom F & u = F . i holds

(ScFS (v,f,F)) . i = (ScProductDM L) . (v,((f . u) * u))

let F be FinSequence of (DivisibleMod L); :: thesis: for v, u being Vector of (DivisibleMod L)

for i being Nat st i in dom F & u = F . i holds

(ScFS (v,f,F)) . i = (ScProductDM L) . (v,((f . u) * u))

let v, u be Vector of (DivisibleMod L); :: thesis: for i being Nat st i in dom F & u = F . i holds

(ScFS (v,f,F)) . i = (ScProductDM L) . (v,((f . u) * u))

let i be Nat; :: thesis: ( i in dom F & u = F . i implies (ScFS (v,f,F)) . i = (ScProductDM L) . (v,((f . u) * u)) )

assume A1: ( i in dom F & u = F . i ) ; :: thesis: (ScFS (v,f,F)) . i = (ScProductDM L) . (v,((f . u) * u))

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

len (ScFS (v,f,F)) = len F by defScFSDM;

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

hence (ScFS (v,f,F)) . i = (ScProductDM L) . (v,((f . u) * u)) by A1, A2, defScFSDM; :: thesis: verum

for F being FinSequence of (DivisibleMod L)

for v, u being Vector of (DivisibleMod L)

for i being Nat st i in dom F & u = F . i holds

(ScFS (v,f,F)) . i = (ScProductDM L) . (v,((f . u) * u))

let f be Function of (DivisibleMod L),INT.Ring; :: thesis: for F being FinSequence of (DivisibleMod L)

for v, u being Vector of (DivisibleMod L)

for i being Nat st i in dom F & u = F . i holds

(ScFS (v,f,F)) . i = (ScProductDM L) . (v,((f . u) * u))

let F be FinSequence of (DivisibleMod L); :: thesis: for v, u being Vector of (DivisibleMod L)

for i being Nat st i in dom F & u = F . i holds

(ScFS (v,f,F)) . i = (ScProductDM L) . (v,((f . u) * u))

let v, u be Vector of (DivisibleMod L); :: thesis: for i being Nat st i in dom F & u = F . i holds

(ScFS (v,f,F)) . i = (ScProductDM L) . (v,((f . u) * u))

let i be Nat; :: thesis: ( i in dom F & u = F . i implies (ScFS (v,f,F)) . i = (ScProductDM L) . (v,((f . u) * u)) )

assume A1: ( i in dom F & u = F . i ) ; :: thesis: (ScFS (v,f,F)) . i = (ScProductDM L) . (v,((f . u) * u))

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

len (ScFS (v,f,F)) = len F by defScFSDM;

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

hence (ScFS (v,f,F)) . i = (ScProductDM L) . (v,((f . u) * u)) by A1, A2, defScFSDM; :: thesis: verum