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
for B being Element of Fin X holds PhiSet (v,(a * f),B) = a * (PhiSet (v,f,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 being Element of (Free_LMod (X,R))
for a being Element of R
for B being Element of Fin X holds PhiSet (v,(a * f),B) = a * (PhiSet (v,f,B))
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
for B being Element of Fin X holds PhiSet (v,(a * f),B) = a * (PhiSet (v,f,B))
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
for B being Element of Fin X holds PhiSet (v,(a * f),B) = a * (PhiSet (v,f,B))
let f be Element of (Free_LMod (X,R)); :: thesis: for a being Element of R
for B being Element of Fin X holds PhiSet (v,(a * f),B) = a * (PhiSet (v,f,B))
let a be Element of R; :: thesis: for B being Element of Fin X holds PhiSet (v,(a * f),B) = a * (PhiSet (v,f,B))
let B be Element of Fin X; :: thesis: PhiSet (v,(a * f),B) = a * (PhiSet (v,f,B))
set F = the addF of N;
set t = TermFS (f,v);
deffunc H₁( Element of N) -> Element of the carrier of N = a * $1;
consider h being Function of the carrier of N, the carrier of N such that
A1: for y being Element of N holds h . y = H₁(y) from FUNCT_2:sch 4();
A2: ( the addF of N is commutative & the addF of N is associative & the addF of N is having_a_unity ) by FVSUM_1:8;
set e = the_unity_wrt the addF of N;
the_unity_wrt the addF of N = 0. N by Lm27;
then A4: h . (the_unity_wrt the addF of N) = a * (0. N) by A1
.= 0. N by VECTSP_1:14
.= the_unity_wrt the addF of N by Lm27 ;
A5: for d1, d2 being Element of N holds h . ( the addF of N . (d1,d2)) = the addF of N . ((h . d1),(h . d2))

proof

let d1, d2 be Element of N; :: thesis: h . ( the addF of N . (d1,d2)) = the addF of N . ((h . d1),(h . d2))
h . ( the addF of N . (d1,d2)) = a * (d1 + d2) by A1
.= (a * d1) + (a * d2) by VECTSP_1:def 14
.= (h . d1) + (a * d2) by A1
.= the addF of N . ((h . d1),(h . d2)) by A1 ;
hence h . ( the addF of N . (d1,d2)) = the addF of N . ((h . d1),(h . d2)) ; :: thesis: verum

end;

h * (TermFS (f,v)) = TermFS ((a * f),v)

proof

for x being Element of X holds (h * (TermFS (f,v))) . x = (TermFS ((a * f),v)) . x

proof

let x be Element of X; :: thesis: (h * (TermFS (f,v))) . x = (TermFS ((a * f),v)) . x
(h * (TermFS (f,v))) . x = h . ((TermFS (f,v)) . x) by FUNCT_2:15
.= a * ((TermFS (f,v)) . x) by A1
.= (TermFS ((a * f),v)) . x by Lm33 ;
hence (h * (TermFS (f,v))) . x = (TermFS ((a * f),v)) . x ; :: thesis: verum

end;

hence h * (TermFS (f,v)) = TermFS ((a * f),v) ; :: thesis: verum

end;

then PhiSet (v,(a * f),B) = h . (PhiSet (v,f,B)) by A2, A4, A5, SETWOP_2:16
.= a * (PhiSet (v,f,B)) by A1 ;
hence PhiSet (v,(a * f),B) = a * (PhiSet (v,f,B)) ; :: thesis: verum