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

for v, u being Vector of (DivisibleMod L) holds ScFS (v,f,<*u*>) = <*((ScProductDM L) . (v,((f . u) * u)))*>

let f be Function of (DivisibleMod L),INT.Ring; :: thesis: for v, u being Vector of (DivisibleMod L) holds ScFS (v,f,<*u*>) = <*((ScProductDM L) . (v,((f . u) * u)))*>

let v, u be Vector of (DivisibleMod L); :: thesis: ScFS (v,f,<*u*>) = <*((ScProductDM L) . (v,((f . u) * u)))*>

A1: 1 in {1} by TARSKI:def 1;

A2: len (ScFS (v,f,<*u*>)) = len <*u*> by defScFSDM

.= 1 by FINSEQ_1:40 ;

then dom (ScFS (v,f,<*u*>)) = {1} by FINSEQ_1:2, FINSEQ_1:def 3;

then (ScFS (v,f,<*u*>)) . 1 = (ScProductDM L) . (v,((f . (<*u*> /. 1)) * (<*u*> /. 1))) by A1, defScFSDM

.= (ScProductDM L) . (v,((f . (<*u*> /. 1)) * u)) by FINSEQ_4:16

.= (ScProductDM L) . (v,((f . u) * u)) by FINSEQ_4:16 ;

hence ScFS (v,f,<*u*>) = <*((ScProductDM L) . (v,((f . u) * u)))*> by A2, FINSEQ_1:40; :: thesis: verum

for v, u being Vector of (DivisibleMod L) holds ScFS (v,f,<*u*>) = <*((ScProductDM L) . (v,((f . u) * u)))*>

let f be Function of (DivisibleMod L),INT.Ring; :: thesis: for v, u being Vector of (DivisibleMod L) holds ScFS (v,f,<*u*>) = <*((ScProductDM L) . (v,((f . u) * u)))*>

let v, u be Vector of (DivisibleMod L); :: thesis: ScFS (v,f,<*u*>) = <*((ScProductDM L) . (v,((f . u) * u)))*>

A1: 1 in {1} by TARSKI:def 1;

A2: len (ScFS (v,f,<*u*>)) = len <*u*> by defScFSDM

.= 1 by FINSEQ_1:40 ;

then dom (ScFS (v,f,<*u*>)) = {1} by FINSEQ_1:2, FINSEQ_1:def 3;

then (ScFS (v,f,<*u*>)) . 1 = (ScProductDM L) . (v,((f . (<*u*> /. 1)) * (<*u*> /. 1))) by A1, defScFSDM

.= (ScProductDM L) . (v,((f . (<*u*> /. 1)) * u)) by FINSEQ_4:16

.= (ScProductDM L) . (v,((f . u) * u)) by FINSEQ_4:16 ;

hence ScFS (v,f,<*u*>) = <*((ScProductDM L) . (v,((f . u) * u)))*> by A2, FINSEQ_1:40; :: thesis: verum