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))
for B being Element of Fin X holds (PhiSet (v,f,B)) + (PhiSet (v,g,B)) = PhiSet (v,(f + g),B)
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))
for B being Element of Fin X holds (PhiSet (v,f,B)) + (PhiSet (v,g,B)) = PhiSet (v,(f + g),B)
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))
for B being Element of Fin X holds (PhiSet (v,f,B)) + (PhiSet (v,g,B)) = PhiSet (v,(f + g),B)
let v be Function of X, the carrier of N; :: thesis: for f, g being Element of (Free_LMod (X,R))
for B being Element of Fin X holds (PhiSet (v,f,B)) + (PhiSet (v,g,B)) = PhiSet (v,(f + g),B)
let f, g be Element of (Free_LMod (X,R)); :: thesis: for B being Element of Fin X holds (PhiSet (v,f,B)) + (PhiSet (v,g,B)) = PhiSet (v,(f + g),B)
let B be Element of Fin X; :: thesis: (PhiSet (v,f,B)) + (PhiSet (v,g,B)) = PhiSet (v,(f + g),B)
set F = the addF of N;
set th = TermFS ((f + g),v);
A1: for x being Element of X st x in B holds
(TermFS ((f + g),v)) . x = ( the addF of N .: ((TermFS (f,v)),(TermFS (g,v)))) . x

proof

let x be Element of X; :: thesis: ( x in B implies (TermFS ((f + g),v)) . x = ( the addF of N .: ((TermFS (f,v)),(TermFS (g,v)))) . x )
(TermFS ((f + g),v)) . x = ((TermFS (f,v)) . x) + ((TermFS (g,v)) . x) by Lm31
.= ( the addF of N .: ((TermFS (f,v)),(TermFS (g,v)))) . x by FUNCOP_1:37 ;
hence ( x in B implies (TermFS ((f + g),v)) . x = ( the addF of N .: ((TermFS (f,v)),(TermFS (g,v)))) . x ) ; :: thesis: verum

end;

(PhiSet (v,f,B)) + (PhiSet (v,g,B)) = the addF of N $$ (B,( the addF of N .: ((TermFS (f,v)),(TermFS (g,v))))) by FVSUM_1:8, SETWOP_2:10
.= PhiSet (v,(f + g),B) by FVSUM_1:8, A1, Th18 ;
hence (PhiSet (v,f,B)) + (PhiSet (v,g,B)) = PhiSet (v,(f + g),B) ; :: thesis: verum