let X be set ; :: thesis: for f2, f1 being FinSequence of REAL st f2 = f1 * (Sgm X) & (dom f1) \ (f1 " {0 }) c= X & X c= dom f1 holds
Sum f1 = Sum f2
let f2, f1 be FinSequence of REAL ; :: thesis: ( f2 = f1 * (Sgm X) & (dom f1) \ (f1 " {0 }) c= X & X c= dom f1 implies Sum f1 = Sum f2 )
assume A1: f2 = f1 * (Sgm X) ; :: thesis: ( not (dom f1) \ (f1 " {0 }) c= X or not X c= dom f1 or Sum f1 = Sum f2 )
assume A2: (dom f1) \ (f1 " {0 }) c= X ; :: thesis: ( not X c= dom f1 or Sum f1 = Sum f2 )
assume A3: X c= dom f1 ; :: thesis: Sum f1 = Sum f2
set Y = (dom f1) \ X;

per cases ( (dom f1) \ X = {} or (dom f1) \ X <> {} ) ;

suppose A4: (dom f1) \ X = {} ; :: thesis: Sum f1 = Sum f2

X \ (dom f1) = {} by A3, XBOOLE_1:37;
then X = dom f1 by A4, XBOOLE_1:32;
then X = Seg (len f1) by FINSEQ_1:def 3;
then Sgm X = idseq (len f1) by FINSEQ_3:54;
hence Sum f1 = Sum f2 by A1, FINSEQ_2:64; :: thesis: verum

end;

suppose A5: (dom f1) \ X <> {} ; :: thesis: Sum f1 = Sum f2

A6: X \/ ((dom f1) \ X) = dom f1 by A3, XBOOLE_1:45;
A7: X misses (dom f1) \ X by XBOOLE_1:79;
set f3 = f1 * (Sgm ((dom f1) \ X));
A8: (dom f1) \ X c= dom f1 by XBOOLE_1:36;
then A9: (dom f1) \ X c= Seg (len f1) by FINSEQ_1:def 3;
then rng (Sgm ((dom f1) \ X)) c= dom f1 by A8, FINSEQ_1:def 13;
then reconsider f3 = f1 * (Sgm ((dom f1) \ X)) as FinSequence of REAL by Th9;
A10: dom f3 = Seg (len f3) by FINSEQ_1:def 3;
A11: (dom f1) \ X c= f1 " {0 }

proof

assume not (dom f1) \ X c= f1 " {0 } ; :: thesis: contradiction
then consider x being set such that
A12: ( x in (dom f1) \ X & not x in f1 " {0 } ) by TARSKI:def 3;
( x in dom f1 & not x in X ) by A12, XBOOLE_0:def 5;
then x in (dom f1) \ (f1 " {0 }) by A12, XBOOLE_0:def 5;
then x in X /\ ((dom f1) \ X) by A2, A12, XBOOLE_0:def 4;
hence contradiction by A7, XBOOLE_0:def 7; :: thesis: verum

end;

for y being set holds
( y in rng f3 iff y = 0 )

proof

let y be set ; :: thesis: ( y in rng f3 iff y = 0 )

hereby :: thesis: ( y = 0 implies y in rng f3 )

assume y in rng f3 ; :: thesis: y = 0
then consider x being set such that
A13: ( x in dom f3 & y = f3 . x ) by FUNCT_1:def 5;
A14: ( x in dom (Sgm ((dom f1) \ X)) & (Sgm ((dom f1) \ X)) . x in dom f1 ) by A13, FUNCT_1:21;
then (Sgm ((dom f1) \ X)) . x in rng (Sgm ((dom f1) \ X)) by FUNCT_1:12;
then (Sgm ((dom f1) \ X)) . x in (dom f1) \ X by A9, FINSEQ_1:def 13;
then f1 . ((Sgm ((dom f1) \ X)) . x) in {0 } by A11, FUNCT_1:def 13;
then f3 . x in {0 } by A14, FUNCT_1:23;
hence y = 0 by A13, TARSKI:def 1; :: thesis: verum

end;

assume A15: y = 0 ; :: thesis: y in rng f3
consider x being set such that
A16: x in (dom f1) \ X by A5, XBOOLE_0:def 1;
A17: ( x in dom f1 & f1 . x in {0 } ) by A16, A11, FUNCT_1:def 13;
x in rng (Sgm ((dom f1) \ X)) by A16, A9, FINSEQ_1:def 13;
then consider x' being set such that
A18: ( x' in dom (Sgm ((dom f1) \ X)) & x = (Sgm ((dom f1) \ X)) . x' ) by FUNCT_1:def 5;
A19: x' in dom f3 by A17, A18, FUNCT_1:21;
f1 . ((Sgm ((dom f1) \ X)) . x') = y by A15, A17, A18, TARSKI:def 1;
then f3 . x' = y by A18, FUNCT_1:23;
hence y in rng f3 by A19, FUNCT_1:def 5; :: thesis: verum

end;

then rng f3 = {0 } by TARSKI:def 1;
then f3 = (Seg (len f3)) --> 0 by A10, FUNCOP_1:15;
then A20: f3 = (len f3) |-> 0 by FINSEQ_2:def 2;
0 is Element of NAT by ORDINAL1:def 13;
then reconsider f3 = f3 as FinSequence of NAT by A20, FINSEQ_2:77;
A21: Sum f3 = 0 by A20, BAGORDER:5;
Sum f1 = (Sum f2) + (Sum f3) by Th10, A6, A1, XBOOLE_1:79;
hence Sum f1 = Sum f2 by A21; :: thesis: verum

end;

end;