let R be non degenerated Ring; :: thesis: FS_Funcs ({},R) = TrivialLMod R
A1: the carrier of (FS_Funcs ({},R)) = the carrier of (TrivialLMod R) by LmTriv;
the addF of (FS_Funcs ({},R)) = op2 by LmTriv2;
hence FS_Funcs ({},R) = TrivialLMod R by A1, LmTriv2; :: thesis: verum