let X be set ; :: thesis: for f1, f2 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 f1, f2 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 )
set Y = (dom f1) \ X;
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

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:48;
hence Sum f1 = Sum f2 by A1, FINSEQ_2:54; :: thesis: verum

end;

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

set f3 = f1 * (Sgm ((dom f1) \ X));
A6: (dom f1) \ X c= dom f1 by XBOOLE_1:36;
A7: rng (Sgm ((dom f1) \ X)) = (dom f1) \ X by FINSEQ_1:def 14;
then reconsider f3 = f1 * (Sgm ((dom f1) \ X)) as FinSequence of REAL by A6, Th9;
A8: X misses (dom f1) \ X by XBOOLE_1:79;
A9: (dom f1) \ X c= f1 " {0}

proof

assume not (dom f1) \ X c= f1 " {0} ; :: thesis: contradiction
then consider x being object such that
A10: x in (dom f1) \ X and
A11: not x in f1 " {0} ;
x in dom f1 by A10, XBOOLE_0:def 5;
then x in (dom f1) \ (f1 " {0}) by A11, XBOOLE_0:def 5;
then x in X /\ ((dom f1) \ X) by A2, A10, XBOOLE_0:def 4;
hence contradiction by A8, XBOOLE_0:def 7; :: thesis: verum

end;

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

proof

let y be object ; :: thesis: ( y in rng f3 iff y = 0 )
consider x being object such that
A12: x in (dom f1) \ X by A5, XBOOLE_0:def 1;

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

assume y in rng f3 ; :: thesis: y = 0
then consider x being object such that
A13: x in dom f3 and
A14: y = f3 . x by FUNCT_1:def 3;
A15: x in dom (Sgm ((dom f1) \ X)) by A13, FUNCT_1:11;
then (Sgm ((dom f1) \ X)) . x in rng (Sgm ((dom f1) \ X)) by FUNCT_1:3;
then (Sgm ((dom f1) \ X)) . x in (dom f1) \ X by FINSEQ_1:def 14;
then f1 . ((Sgm ((dom f1) \ X)) . x) in {0} by A9, FUNCT_1:def 7;
then f3 . x in {0} by A15, FUNCT_1:13;
hence y = 0 by A14, TARSKI:def 1; :: thesis: verum

end;

assume A16: y = 0 ; :: thesis: y in rng f3
x in rng (Sgm ((dom f1) \ X)) by A7, A12;
then consider x9 being object such that
A17: x9 in dom (Sgm ((dom f1) \ X)) and
A18: x = (Sgm ((dom f1) \ X)) . x9 by FUNCT_1:def 3;
f1 . x in {0} by A9, A12, FUNCT_1:def 7;
then f1 . ((Sgm ((dom f1) \ X)) . x9) = y by A16, A18, TARSKI:def 1;
then A19: f3 . x9 = y by A17, FUNCT_1:13;
x in dom f1 by A9, A12, FUNCT_1:def 7;
then x9 in dom f3 by A17, A18, FUNCT_1:11;
hence y in rng f3 by A19, FUNCT_1:def 3; :: thesis: verum

end;

then ( dom f3 = Seg (len f3) & rng f3 = {0} ) by FINSEQ_1:def 3, TARSKI:def 1;
then f3 = (Seg (len f3)) --> 0 by FUNCOP_1:9;
then A20: f3 = (len f3) |-> 0 by FINSEQ_2:def 2;
then reconsider f3 = f3 as FinSequence of NAT ;
X \/ ((dom f1) \ X) = dom f1 by A3, XBOOLE_1:45;
then A21: Sum f1 = (Sum f2) + (Sum f3) by A1, Th10, XBOOLE_1:79;
Sum f3 = 0 by A20, BAGORDER:4;
hence Sum f1 = Sum f2 by A21; :: thesis: verum

end;

end;