let R be Ring; :: thesis: for X being set
for f, g being finite-Support Function of X, the carrier of R holds (ADD (X,R)) . [f,g] is finite-Support Function of X, the carrier of R
let X be set ; :: thesis: for f, g being finite-Support Function of X, the carrier of R holds (ADD (X,R)) . [f,g] is finite-Support Function of X, the carrier of R
let f, g be finite-Support Function of X, the carrier of R; :: thesis: (ADD (X,R)) . [f,g] is finite-Support Function of X, the carrier of R
reconsider f1 = f, g1 = g as Element of Funcs (X, the carrier of R) by FUNCT_2:8;
reconsider h = (ADD (X,R)) . (f1,g1) as Element of Funcs (X, the carrier of R) ;
for o being object st o in Support h holds
o in (Support f1) \/ (Support g1)

proof

let o be object ; :: thesis: ( o in Support h implies o in (Support f1) \/ (Support g1) )
assume A1: o in Support h ; :: thesis: o in (Support f1) \/ (Support g1)
set x = o;
A2: o in dom h by A1, POLYNOM1:def 3;
A3: dom h = X by FUNCT_2:def 1;
A4: ( dom f1 = X & dom g1 = X ) by FUNCT_2:def 1;
assume not o in (Support f1) \/ (Support g1) ; :: thesis: contradiction
then ( not o in Support f1 & not o in Support g1 ) by XBOOLE_0:def 3;
then A6: ( f1 . o = 0. R & g1 . o = 0. R ) by A2, A4, POLYNOM1:def 3;
A8: o in dom ( the addF of R .: (f1,g1)) by A2, A3, FUNCT_2:def 1;
h . o = ( the addF of R .: (f1,g1)) . o by Def6
.= (0. R) + (0. R) by A6, A8, FUNCOP_1:22
.= 0. R ;
hence contradiction by A1, POLYNOM1:def 3; :: thesis: verum

end;

then A5: Support h c= (Support f1) \/ (Support g1) ;
( Support f1 is finite & Support g1 is finite ) by POLYNOM1:def 5;
hence (ADD (X,R)) . [f,g] is finite-Support Function of X, the carrier of R by A5, POLYNOM1:def 5; :: thesis: verum