let L be Z_Lattice; :: thesis: for f being Function of L,INT.Ring
for F being FinSequence of L
for v, u being Vector of L
for i being Nat st i in dom F & u = F . i holds
(ScFS (v,f,F)) . i = <;v,((f . u) * u);>

let f be Function of L,INT.Ring; :: thesis: for F being FinSequence of L
for v, u being Vector of L
for i being Nat st i in dom F & u = F . i holds
(ScFS (v,f,F)) . i = <;v,((f . u) * u);>

let F be FinSequence of L; :: thesis: for v, u being Vector of L
for i being Nat st i in dom F & u = F . i holds
(ScFS (v,f,F)) . i = <;v,((f . u) * u);>

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

let i be Nat; :: thesis: ( i in dom F & u = F . i implies (ScFS (v,f,F)) . i = <;v,((f . u) * u);> )
assume A1: ( i in dom F & u = F . i ) ; :: thesis: (ScFS (v,f,F)) . i = <;v,((f . u) * u);>
A2: F /. i = F . i by ;
len (ScFS (v,f,F)) = len F by defScFS;
then i in dom (ScFS (v,f,F)) by ;
hence (ScFS (v,f,F)) . i = <;v,((f . u) * u);> by ; :: thesis: verum