let R be non degenerated Ring; :: thesis: for X being non empty set
for N being LeftMod of R
for v being Function of X, the carrier of N
for f, g being Element of (Free_LMod (X,R)) st Support (@ f) misses Support (@ g) holds
(Phi v) . (f + g) = ((Phi v) . f) + ((Phi v) . g)
let X be non empty set ; :: thesis: for N being LeftMod of R
for v being Function of X, the carrier of N
for f, g being Element of (Free_LMod (X,R)) st Support (@ f) misses Support (@ g) holds
(Phi v) . (f + g) = ((Phi v) . f) + ((Phi v) . g)
let N be LeftMod of R; :: thesis: for v being Function of X, the carrier of N
for f, g being Element of (Free_LMod (X,R)) st Support (@ f) misses Support (@ g) holds
(Phi v) . (f + g) = ((Phi v) . f) + ((Phi v) . g)
let v be Function of X, the carrier of N; :: thesis: for f, g being Element of (Free_LMod (X,R)) st Support (@ f) misses Support (@ g) holds
(Phi v) . (f + g) = ((Phi v) . f) + ((Phi v) . g)
let f, g be Element of (Free_LMod (X,R)); :: thesis: ( Support (@ f) misses Support (@ g) implies (Phi v) . (f + g) = ((Phi v) . f) + ((Phi v) . g) )
assume A1: Support (@ f) misses Support (@ g) ; :: thesis: (Phi v) . (f + g) = ((Phi v) . f) + ((Phi v) . g)
set F = the addF of N;
set Bf = SuppFin f;
set Bg = SuppFin g;
set tf = TermFS (f,v);
set tg = TermFS (g,v);
set th = TermFS ((f + g),v);
A2: for x being Element of X st x in SuppFin f holds
(TermFS ((f + g),v)) . x = (TermFS (f,v)) . x

proof

let x be Element of X; :: thesis: ( x in SuppFin f implies (TermFS ((f + g),v)) . x = (TermFS (f,v)) . x )
assume x in SuppFin f ; :: thesis: (TermFS ((f + g),v)) . x = (TermFS (f,v)) . x
then A4: not x in Support (@ g) by A1, XBOOLE_0:3;
(TermFS ((f + g),v)) . x = ((@ (f + g)) . x) * (v . x) by Def28
.= (((@ f) . x) + ((@ g) . x)) * (v . x) by Th8
.= (((@ f) . x) + (0. R)) * (v . x) by A4, POLYNOM1:def 4
.= (TermFS (f,v)) . x by Def28 ;
hence (TermFS ((f + g),v)) . x = (TermFS (f,v)) . x ; :: thesis: verum

end;

A5: for x being Element of X st x in SuppFin g holds
(TermFS ((f + g),v)) . x = (TermFS (g,v)) . x

proof

let x be Element of X; :: thesis: ( x in SuppFin g implies (TermFS ((f + g),v)) . x = (TermFS (g,v)) . x )
assume x in SuppFin g ; :: thesis: (TermFS ((f + g),v)) . x = (TermFS (g,v)) . x
then A7: not x in Support (@ f) by A1, XBOOLE_0:3;
(TermFS ((f + g),v)) . x = ((@ (f + g)) . x) * (v . x) by Def28
.= (((@ f) . x) + ((@ g) . x)) * (v . x) by Th8
.= ((0. R) + ((@ g) . x)) * (v . x) by A7, POLYNOM1:def 4
.= (TermFS (g,v)) . x by Def28 ;
hence (TermFS ((f + g),v)) . x = (TermFS (g,v)) . x ; :: thesis: verum

end;

A8: PhiSet (v,(f + g),(SuppFin g)) = PhiSet (v,g,(SuppFin g)) by FVSUM_1:8, A5, Th18;
(Phi v) . (f + g) = PhiSet (v,(f + g),(SuppFin (f + g))) by Def31
.= PhiSet (v,(f + g),((SuppFin f) \/ (SuppFin g))) by A1, Th16
.= the addF of N . ((PhiSet (v,(f + g),(SuppFin f))),(PhiSet (v,(f + g),(SuppFin g)))) by A1, FVSUM_1:8, SETWOP_2:4
.= the addF of N . ((PhiSet (v,f,(SuppFin f))),(PhiSet (v,g,(SuppFin g)))) by FVSUM_1:8, A2, Th18, A8
.= the addF of N . (((Phi v) . f),(PhiSet (v,g,(SuppFin g)))) by Def31
.= ((Phi v) . f) + ((Phi v) . g) by Def31 ;
hence (Phi v) . (f + g) = ((Phi v) . f) + ((Phi v) . g) ; :: thesis: verum