let L be Z_Lattice; :: thesis: for f being Function of L,INT.Ring
for v, u being Vector of L holds ScFS (v,f,<*u*>) = <*<;v,((f . u) * u);>*>
let f be Function of L,INT.Ring; :: thesis: for v, u being Vector of L holds ScFS (v,f,<*u*>) = <*<;v,((f . u) * u);>*>
let v, u be Vector of L; :: thesis: ScFS (v,f,<*u*>) = <*<;v,((f . u) * u);>*>
A1: 1 in {1} by TARSKI:def 1;
A2: len (ScFS (v,f,<*u*>)) = len <*u*> by defScFS
.= 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 = <;v,((f . (<*u*> /. 1)) * (<*u*> /. 1));> by A1, defScFS
.= <;v,((f . (<*u*> /. 1)) * u);> by FINSEQ_4:16
.= <;v,((f . u) * u);> by FINSEQ_4:16 ;
hence ScFS (v,f,<*u*>) = <*<;v,((f . u) * u);>*> by A2, FINSEQ_1:40; :: thesis: verum