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)) 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)) 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)) 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)) holds (Phi v) . (f + g) = ((Phi v) . f) + ((Phi v) . g)
let f, g be Element of (Free_LMod (X,R)); :: thesis: (Phi v) . (f + g) = ((Phi v) . f) + ((Phi v) . g)
set Bf = SuppFin f;
set Bg = SuppFin g;
set Bh = SuppFin (f + g);
set B = (SuppFin f) \/ (SuppFin g);
A1: SuppFin (f + g) c= (SuppFin f) \/ (SuppFin g) by Lm30;
A2: PhiSet (v,f,(SuppFin f)) = PhiSet (v,f,((SuppFin f) \/ (SuppFin g)))

proof

for x being Element of X st x in ((SuppFin f) \/ (SuppFin g)) \ (SuppFin f) holds
(TermFS (f,v)) . x = 0. N

proof

let x be Element of X; :: thesis: ( x in ((SuppFin f) \/ (SuppFin g)) \ (SuppFin f) implies (TermFS (f,v)) . x = 0. N )
assume x in ((SuppFin f) \/ (SuppFin g)) \ (SuppFin f) ; :: thesis: (TermFS (f,v)) . x = 0. N
then not x in SuppFin f by XBOOLE_0:def 5;
hence (TermFS (f,v)) . x = 0. N by Lm29; :: thesis: verum

end;

hence PhiSet (v,f,(SuppFin f)) = PhiSet (v,f,((SuppFin f) \/ (SuppFin g))) by XBOOLE_1:7, Lm28; :: thesis: verum

end;

A4: PhiSet (v,g,(SuppFin g)) = PhiSet (v,g,((SuppFin f) \/ (SuppFin g)))

proof

for x being Element of X st x in ((SuppFin f) \/ (SuppFin g)) \ (SuppFin g) holds
(TermFS (g,v)) . x = 0. N

proof

let x be Element of X; :: thesis: ( x in ((SuppFin f) \/ (SuppFin g)) \ (SuppFin g) implies (TermFS (g,v)) . x = 0. N )
assume x in ((SuppFin f) \/ (SuppFin g)) \ (SuppFin g) ; :: thesis: (TermFS (g,v)) . x = 0. N
then not x in SuppFin g by XBOOLE_0:def 5;
hence (TermFS (g,v)) . x = 0. N by Lm29; :: thesis: verum

end;

hence PhiSet (v,g,(SuppFin g)) = PhiSet (v,g,((SuppFin f) \/ (SuppFin g))) by XBOOLE_1:7, Lm28; :: thesis: verum

end;

A6: PhiSet (v,(f + g),(SuppFin (f + g))) = PhiSet (v,(f + g),((SuppFin f) \/ (SuppFin g)))

proof

for x being Element of X st x in ((SuppFin f) \/ (SuppFin g)) \ (SuppFin (f + g)) holds
(TermFS ((f + g),v)) . x = 0. N

proof

let x be Element of X; :: thesis: ( x in ((SuppFin f) \/ (SuppFin g)) \ (SuppFin (f + g)) implies (TermFS ((f + g),v)) . x = 0. N )
assume x in ((SuppFin f) \/ (SuppFin g)) \ (SuppFin (f + g)) ; :: thesis: (TermFS ((f + g),v)) . x = 0. N
then not x in SuppFin (f + g) by XBOOLE_0:def 5;
hence (TermFS ((f + g),v)) . x = 0. N by Lm29; :: thesis: verum

end;

hence PhiSet (v,(f + g),(SuppFin (f + g))) = PhiSet (v,(f + g),((SuppFin f) \/ (SuppFin g))) by A1, Lm28; :: thesis: verum

end;

(Phi v) . (f + g) = PhiSet (v,(f + g),((SuppFin f) \/ (SuppFin g))) by A6, Def31
.= (PhiSet (v,f,(SuppFin f))) + (PhiSet (v,g,(SuppFin g))) by A4, A2, Lm32
.= ((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