let R be non degenerated Ring; :: thesis: for X being non empty set
for x being Element of X holds
( iota (x,R) in fs_Funcs (X,R) & iota (x,R) is finite-Support Function of X, the carrier of R )
let X be non empty set ; :: thesis: for x being Element of X holds
( iota (x,R) in fs_Funcs (X,R) & iota (x,R) is finite-Support Function of X, the carrier of R )
let x be Element of X; :: thesis: ( iota (x,R) in fs_Funcs (X,R) & iota (x,R) is finite-Support Function of X, the carrier of R )
set f = iota (x,R);
Support (iota (x,R)) = {x} by Lm16;
then iota (x,R) is finite-Support Function of X, the carrier of R by POLYNOM1:def 5;
hence ( iota (x,R) in fs_Funcs (X,R) & iota (x,R) is finite-Support Function of X, the carrier of R ) ; :: thesis: verum