let R be Ring; :: thesis: for X being set
for a being Element of R
for f being Element of Funcs (X, the carrier of R) st f in fs_Funcs (X,R) holds
(LMULT (X,R)) . (a,f) in fs_Funcs (X,R)
let X be set ; :: thesis: for a being Element of R
for f being Element of Funcs (X, the carrier of R) st f in fs_Funcs (X,R) holds
(LMULT (X,R)) . (a,f) in fs_Funcs (X,R)
let a be Element of R; :: thesis: for f being Element of Funcs (X, the carrier of R) st f in fs_Funcs (X,R) holds
(LMULT (X,R)) . (a,f) in fs_Funcs (X,R)
let f be Element of Funcs (X, the carrier of R); :: thesis: ( f in fs_Funcs (X,R) implies (LMULT (X,R)) . (a,f) in fs_Funcs (X,R) )
assume f in fs_Funcs (X,R) ; :: thesis: (LMULT (X,R)) . (a,f) 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 ) ;
(LMULT (X,R)) . (a,f) is finite-Support Function of X, the carrier of R by A2, Th4;
hence (LMULT (X,R)) . (a,f) in fs_Funcs (X,R) ; :: thesis: verum