let R be non degenerated Ring; :: thesis: ( fs_ADD ({},R) = op2 & fs_LMULT ({},R) = pr2 ( the carrier of R,{0}) )
fs_Funcs ({},R) = {{}} by LmTriv;
hence ( fs_ADD ({},R) = op2 & fs_LMULT ({},R) = pr2 ( the carrier of R,{0}) ) by FUNCT_2:51; :: thesis: verum