let X be non empty set ; :: thesis: for R being non degenerated Ring
for f, g being Element of (Free_LMod (X,R)) st Support (@ f) misses Support (@ g) holds
Support (@ (f + g)) = (Support (@ f)) \/ (Support (@ g))
let R be non degenerated Ring; :: thesis: for f, g being Element of (Free_LMod (X,R)) st Support (@ f) misses Support (@ g) holds
Support (@ (f + g)) = (Support (@ f)) \/ (Support (@ g))
let f, g be Element of (Free_LMod (X,R)); :: thesis: ( Support (@ f) misses Support (@ g) implies Support (@ (f + g)) = (Support (@ f)) \/ (Support (@ g)) )
assume A1: Support (@ f) misses Support (@ g) ; :: thesis: Support (@ (f + g)) = (Support (@ f)) \/ (Support (@ g))
thus Support (@ (f + g)) c= (Support (@ f)) \/ (Support (@ g)) :: according to XBOOLE_0:def 10 :: thesis: (Support (@ f)) \/ (Support (@ g)) c= Support (@ (f + g))

proof

let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in Support (@ (f + g)) or o in (Support (@ f)) \/ (Support (@ g)) )
assume A3: o in Support (@ (f + g)) ; :: thesis: o in (Support (@ f)) \/ (Support (@ g))
then reconsider x = o as Element of X ;
x in (Support (@ f)) \/ (Support (@ g))

proof

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 A5: ( (@ f) . x = 0. R & (@ g) . x = 0. R ) by POLYNOM1:def 4;
(@ (f + g)) . x = ((@ f) . x) + ((@ g) . x) by Th8
.= 0. R by A5 ;
hence contradiction by A3, POLYNOM1:def 4; :: thesis: verum

end;

hence o in (Support (@ f)) \/ (Support (@ g)) ; :: thesis: verum

end;

let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in (Support (@ f)) \/ (Support (@ g)) or o in Support (@ (f + g)) )
assume o in (Support (@ f)) \/ (Support (@ g)) ; :: thesis: o in Support (@ (f + g))

per cases then ( o in Support (@ f) or o in Support (@ g) ) by XBOOLE_0:def 3;

suppose A7: o in Support (@ f) ; :: thesis: o in Support (@ (f + g))

then reconsider x = o as Element of X ;
A8: (@ (f + g)) . x = ((@ f) . x) + ((@ g) . x) by Th8;
not x in Support (@ g) by A1, A7, XBOOLE_0:def 4;
then (@ g) . x = 0. R by POLYNOM1:def 4;
then 0. R <> ((@ f) . x) + ((@ g) . x) by A7, POLYNOM1:def 4;
hence o in Support (@ (f + g)) by A8, POLYNOM1:def 4; :: thesis: verum

end;

suppose A10: o in Support (@ g) ; :: thesis: o in Support (@ (f + g))

then reconsider x = o as Element of X ;
A11: (@ (f + g)) . x = ((@ f) . x) + ((@ g) . x) by Th8;
not x in Support (@ f) by A1, A10, XBOOLE_0:def 4;
then (@ f) . x = 0. R by POLYNOM1:def 4;
then 0. R <> ((@ f) . x) + ((@ g) . x) by A10, POLYNOM1:def 4;
hence o in Support (@ (f + g)) by A11, POLYNOM1:def 4; :: thesis: verum

end;

end;