let R be Ring; :: thesis: for X being set
for f, g being Element of Funcs (X, the carrier of R) st f in fs_Funcs (X,R) & g in fs_Funcs (X,R) holds
(ADD (X,R)) . [f,g] in fs_Funcs (X,R)
let X be set ; :: thesis: for f, g being Element of Funcs (X, the carrier of R) st f in fs_Funcs (X,R) & g in fs_Funcs (X,R) holds
(ADD (X,R)) . [f,g] in fs_Funcs (X,R)
let f, g be Element of Funcs (X, the carrier of R); :: thesis: ( f in fs_Funcs (X,R) & g in fs_Funcs (X,R) implies (ADD (X,R)) . [f,g] in fs_Funcs (X,R) )
assume A1: ( f in fs_Funcs (X,R) & g in fs_Funcs (X,R) ) ; :: thesis: (ADD (X,R)) . [f,g] in fs_Funcs (X,R)
then consider f1 being Function of X, the carrier of R such that
A2: ( f1 = f & f1 is finite-Support ) ;
consider g1 being Function of X, the carrier of R such that
A3: ( g1 = g & g1 is finite-Support ) by A1;
(ADD (X,R)) . [f,g] is finite-Support Function of X, the carrier of R by Th3, A3, A2;
hence (ADD (X,R)) . [f,g] in fs_Funcs (X,R) ; :: thesis: verum