let R be Ring; :: thesis: for X being set holds 0_Funcs (X,R) in fs_Funcs (X,R)
let X be set ; :: thesis: 0_Funcs (X,R) in fs_Funcs (X,R)
( 0_Funcs (X,R) is Function of X, the carrier of R & 0_Funcs (X,R) is finite-Support ) by Lm8;
hence 0_Funcs (X,R) in fs_Funcs (X,R) ; :: thesis: verum