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 B, C being Element of Fin X st B c= C & ( for x being Element of X st x in C \ B holds
(TermFS (f,v)) . x = 0. N ) holds
PhiSet (v,f,B) = PhiSet (v,f,C)
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 B, C being Element of Fin X st B c= C & ( for x being Element of X st x in C \ B holds
(TermFS (f,v)) . x = 0. N ) holds
PhiSet (v,f,B) = PhiSet (v,f,C)
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 B, C being Element of Fin X st B c= C & ( for x being Element of X st x in C \ B holds
(TermFS (f,v)) . x = 0. N ) holds
PhiSet (v,f,B) = PhiSet (v,f,C)
let v be Function of X, the carrier of N; :: thesis: for f being Element of (Free_LMod (X,R))
for B, C being Element of Fin X st B c= C & ( for x being Element of X st x in C \ B holds
(TermFS (f,v)) . x = 0. N ) holds
PhiSet (v,f,B) = PhiSet (v,f,C)
let f be Element of (Free_LMod (X,R)); :: thesis: for B, C being Element of Fin X st B c= C & ( for x being Element of X st x in C \ B holds
(TermFS (f,v)) . x = 0. N ) holds
PhiSet (v,f,B) = PhiSet (v,f,C)
let B, C be Element of Fin X; :: thesis: ( B c= C & ( for x being Element of X st x in C \ B holds
(TermFS (f,v)) . x = 0. N ) implies PhiSet (v,f,B) = PhiSet (v,f,C) )
assume that
A1: B c= C and
A2: for x being Element of X st x in C \ B holds
(TermFS (f,v)) . x = 0. N ; :: thesis: PhiSet (v,f,B) = PhiSet (v,f,C)
set F = the addF of N;
set t = TermFS (f,v);
reconsider D = C \ B as Element of Fin X ;
A5: C = B \/ D by A1, XBOOLE_1:45;
A6: B misses D by XBOOLE_1:79;

per cases ( D = {} or D <> {} ) ;

suppose D = {} ; :: thesis: PhiSet (v,f,B) = PhiSet (v,f,C)

then C = B by A1, XBOOLE_1:37;
hence PhiSet (v,f,B) = PhiSet (v,f,C) ; :: thesis: verum

end;

suppose A8: D <> {} ; :: thesis: PhiSet (v,f,B) = PhiSet (v,f,C)

A9: (TermFS (f,v)) .: D = {(0. N)}

proof

thus (TermFS (f,v)) .: D c= {(0. N)} :: according to XBOOLE_0:def 10 :: thesis: {(0. N)} c= (TermFS (f,v)) .: D

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in (TermFS (f,v)) .: D or y in {(0. N)} )
assume y in (TermFS (f,v)) .: D ; :: thesis: y in {(0. N)}
then consider x being object such that
A12: ( x in dom (TermFS (f,v)) & x in D & y = (TermFS (f,v)) . x ) by FUNCT_1:def 6;
reconsider x1 = x as Element of X by A12;
(TermFS (f,v)) . x1 = 0. N by A2, A12;
hence y in {(0. N)} by A12, TARSKI:def 1; :: thesis: verum

end;

A14: D is Subset of X by FINSUB_1:16;
consider x being object such that
A15: x in D by A8, XBOOLE_0:def 1;
reconsider x1 = x as Element of X by A15, A14;
ex u being object st
( u in dom (TermFS (f,v)) & u in D & 0. N = (TermFS (f,v)) . u )

proof

take x1 ; :: thesis: ( x1 in dom (TermFS (f,v)) & x1 in D & 0. N = (TermFS (f,v)) . x1 )
dom (TermFS (f,v)) = X by FUNCT_2:def 1;
hence ( x1 in dom (TermFS (f,v)) & x1 in D & 0. N = (TermFS (f,v)) . x1 ) by A15, A2; :: thesis: verum

end;

then A17: 0. N in (TermFS (f,v)) .: D by FUNCT_1:def 6;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in {(0. N)} or y in (TermFS (f,v)) .: D )
assume y in {(0. N)} ; :: thesis: y in (TermFS (f,v)) .: D
hence y in (TermFS (f,v)) .: D by A17, TARSKI:def 1; :: thesis: verum

end;

A19: the addF of N $$ (D,(TermFS (f,v))) = 0. N

proof

set e = the_unity_wrt the addF of N;
(TermFS (f,v)) .: D = {(the_unity_wrt the addF of N)} by A9, Lm27;
then the addF of N $$ (D,(TermFS (f,v))) = the_unity_wrt the addF of N by FVSUM_1:8, SETWOP_2:8
.= 0. N by Lm27 ;
hence the addF of N $$ (D,(TermFS (f,v))) = 0. N ; :: thesis: verum

end;

PhiSet (v,f,C) = ( the addF of N $$ (B,(TermFS (f,v)))) + (0. N) by A19, A6, FVSUM_1:8, A5, SETWOP_2:4
.= PhiSet (v,f,B) ;
hence PhiSet (v,f,B) = PhiSet (v,f,C) ; :: thesis: verum

end;

end;