let R be Ring; :: thesis:
let X be set ; :: thesis:
let a be Element of the carrier of R; :: thesis:
let g be finite-Support Function of X, the carrier of R; :: thesis:
reconsider g = g as Element of Funcs (X, the carrier of R) by FUNCT_2:8;
reconsider F = (LMULT (X,R)) . (a,g) as Element of Funcs (X, the carrier of R) ;
B1: ( dom F = X & dom g = X ) by FUNCT_2:def 1;
A1: Support g is finite by POLYNOM1:def 5;
for o being object st o in Support F holds
o in Support g

let o be object ; :: thesis:
assume A2: o in Support F ; :: thesis:
then A3: o in dom F by POLYNOM1:def 3;
then reconsider x = o as Element of X ;
reconsider gx = g . x as Element of R by A3, FUNCT_2:5;
F . x <> 0. R by A2, POLYNOM1:def 3;
then a * gx <> 0. R by A3, Th2;
then g . x <> 0. R ;
hence o in Support g by A3, B1, POLYNOM1:def 3; :: thesis:

end;