let n be Nat; :: thesis: for g being FinSequence of REAL n
for h being FinSequence of NAT
for F being FinSequence of REAL n st h is one-to-one & rng h c= dom g & F = g * h & ( for i being Element of NAT st i in dom g & not i in rng h holds
g . i = 0* n ) holds
Sum g = Sum F
let g be FinSequence of REAL n; :: thesis: for h being FinSequence of NAT
for F being FinSequence of REAL n st h is one-to-one & rng h c= dom g & F = g * h & ( for i being Element of NAT st i in dom g & not i in rng h holds
g . i = 0* n ) holds
Sum g = Sum F
let h be FinSequence of NAT ; :: thesis: for F being FinSequence of REAL n st h is one-to-one & rng h c= dom g & F = g * h & ( for i being Element of NAT st i in dom g & not i in rng h holds
g . i = 0* n ) holds
Sum g = Sum F
let F be FinSequence of REAL n; :: thesis: ( h is one-to-one & rng h c= dom g & F = g * h & ( for i being Element of NAT st i in dom g & not i in rng h holds
g . i = 0* n ) implies Sum g = Sum F )
assume that
A1: h is one-to-one and
A2: rng h c= dom g and
A3: F = g * h and
A4: for i being Element of NAT st i in dom g & not i in rng h holds
g . i = 0* n ; :: thesis: Sum g = Sum F
consider h3 being Permutation of (dom h), h2 being FinSequence of NAT such that
A5: h2 = h * h3 and
A6: h2 is increasing and
A7: dom h = dom h2 and
A8: rng h = rng h2 by A1, Th13;
dom (g * h) = dom h by A2, RELAT_1:27;
then reconsider h33 = h3 as Permutation of (dom F) by A3;
reconsider F22 = g * h2 as Function ;
dom F22 = dom h by A2, A7, A8, RELAT_1:27
.= Seg (len h) by FINSEQ_1:def 3 ;
then reconsider F23 = F22 as FinSequence by FINSEQ_1:def 2;
rng F22 c= rng g by RELAT_1:26;
then rng F23 c= REAL n by XBOOLE_1:1;
then reconsider F2 = F23 as FinSequence of REAL n by FINSEQ_1:def 4;
F2 = F (*) h33 by A3, A5, RELAT_1:36;
then Sum F = Sum F2 by Th20;
hence Sum g = Sum F by A2, A4, A6, A8, Th22; :: thesis: verum