let R be non degenerated Ring; :: thesis: ( fs_Funcs ({},R) = {{}} & 0_Funcs ({},R) = {} )
A0: Funcs ({}, the carrier of R) = {{}} by FUNCT_5:57;
( 0_Funcs ({},R) is finite-Support & Support (0_Funcs ({},R)) = {} ) by Lm8;
then 0_Funcs ({},R) in fs_Funcs ({},R) ;
then {{}} c= fs_Funcs ({},R) by TARSKI:def 1;
hence ( fs_Funcs ({},R) = {{}} & 0_Funcs ({},R) = {} ) by A0; :: thesis: verum