let R be non degenerated Ring; :: thesis: for X being non empty set
for f, g being Element of (Free_LMod (X,R))
for x being Element of X st x in Support (@ (f + g)) holds
x in (Support (@ f)) \/ (Support (@ g))
let X be non empty set ; :: thesis: for f, g being Element of (Free_LMod (X,R))
for x being Element of X st x in Support (@ (f + g)) holds
x in (Support (@ f)) \/ (Support (@ g))
let f, g be Element of (Free_LMod (X,R)); :: thesis: for x being Element of X st x in Support (@ (f + g)) holds
x in (Support (@ f)) \/ (Support (@ g))
let x be Element of X; :: thesis: ( x in Support (@ (f + g)) implies x in (Support (@ f)) \/ (Support (@ g)) )
assume A1: x in Support (@ (f + g)) ; :: thesis: x in (Support (@ f)) \/ (Support (@ g))
assume not x in (Support (@ f)) \/ (Support (@ g)) ; :: thesis: contradiction
then ( not x in Support (@ f) & not x in Support (@ g) ) by XBOOLE_0:def 3;
then A3: ( (@ f) . x = 0. R & (@ g) . x = 0. R ) by POLYNOM1:def 4;
(@ (f + g)) . x = ((@ f) . x) + ((@ g) . x) by Th8
.= 0. R by A3 ;
hence contradiction by A1, POLYNOM1:def 4; :: thesis: verum