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 being Element of (Free_LMod (X,R))
for a being Element of R holds (Phi v) . (a * f) = a * ((Phi v) . f)
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 being Element of (Free_LMod (X,R))
for a being Element of R holds (Phi v) . (a * f) = a * ((Phi v) . f)
let N be LeftMod of R; :: thesis: for v being Function of X, the carrier of N
for f being Element of (Free_LMod (X,R))
for a being Element of R holds (Phi v) . (a * f) = a * ((Phi v) . f)
let v be Function of X, the carrier of N; :: thesis: for f being Element of (Free_LMod (X,R))
for a being Element of R holds (Phi v) . (a * f) = a * ((Phi v) . f)
let f be Element of (Free_LMod (X,R)); :: thesis: for a being Element of R holds (Phi v) . (a * f) = a * ((Phi v) . f)
let a be Element of R; :: thesis: (Phi v) . (a * f) = a * ((Phi v) . f)
set Bf = SuppFin f;
set Baf = SuppFin (a * f);
set B = (SuppFin f) \/ (SuppFin (a * f));
A1: PhiSet (v,f,(SuppFin f)) = PhiSet (v,f,((SuppFin f) \/ (SuppFin (a * f))))

proof

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

proof

let x be Element of X; :: thesis: ( x in ((SuppFin f) \/ (SuppFin (a * f))) \ (SuppFin f) implies (TermFS (f,v)) . x = 0. N )
assume x in ((SuppFin f) \/ (SuppFin (a * f))) \ (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 (a * f)))) by XBOOLE_1:7, Lm28; :: thesis: verum

end;

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

proof

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

proof

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

end;

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

end;

(Phi v) . (a * f) = PhiSet (v,(a * f),((SuppFin f) \/ (SuppFin (a * f)))) by A4, Def31
.= a * (PhiSet (v,f,(SuppFin f))) by A1, Lm34
.= a * ((Phi v) . f) by Def31 ;
hence (Phi v) . (a * f) = a * ((Phi v) . f) ; :: thesis: verum