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

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