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