let s, m, a be non zero Nat; :: thesis: for f being s -element natural-valued positive-yielding FinSequence
for g being (s + (a |^ m)) - 1 -element natural-valued positive-yielding FinSequence st g = Expand (f,m,a) holds
Sum ((f ") |^ m) = Sum ((g ") |^ m)
let f be s -element natural-valued positive-yielding FinSequence; :: thesis: for g being (s + (a |^ m)) - 1 -element natural-valued positive-yielding FinSequence st g = Expand (f,m,a) holds
Sum ((f ") |^ m) = Sum ((g ") |^ m)
let g be (s + (a |^ m)) - 1 -element natural-valued positive-yielding FinSequence; :: thesis: ( g = Expand (f,m,a) implies Sum ((f ") |^ m) = Sum ((g ") |^ m) )
assume CC: g = Expand (f,m,a) ; :: thesis: Sum ((f ") |^ m) = Sum ((g ") |^ m)
p0: len f = s by CARD_1:def 7;
then AA: f | s = f ;
set t = s -' 1;
set S = Sum (((f | s) ") |^ m);
(s -' 1) + 1 = s by NAT_1:14, XREAL_1:235;
then f = (f | (s -' 1)) ^ <*(f . s)*> by p0, RFINSEQ:7;
then f " = ((f | (s -' 1)) ") ^ (<*(f . s)*> ") by NUMBER15:60;
then (f ") |^ m = (((f | (s -' 1)) ") |^ m) ^ ((<*(f . s)*> ") |^ m) by ConcatPower;
then Sum ((f ") |^ m) = (Sum (((f | (s -' 1)) ") |^ m)) + (Sum ((<*(f . s)*> ") |^ m)) by RVSUM_1:75;
then K1: Sum (((f | (s -' 1)) ") |^ m) = (Sum (((f | s) ") |^ m)) - (Sum ((<*(f . s)*> ") |^ m)) by AA;
set h = (a |^ m) |-> (a * (f . s));
HH: Sum (((((a |^ m) |-> (a * (f . s))) | (a |^ m)) ") |^ m) = (1 / (f . s)) |^ m

proof

len f = s by CARD_1:def 7;
then ( 1 <= s & s <= len f ) by NAT_1:14;
then s in dom f by FINSEQ_3:25;
then f . s in rng f by FUNCT_1:3;
then f . s > 0 by PARTFUN3:def 1;
then S1: 1 / (a * (f . s)) > 0 ;
len (((((a |^ m) |-> (a * (f . s))) | (a |^ m)) ") |^ m) = len ((((a |^ m) |-> (a * (f . s))) | (a |^ m)) ") by NAT_3:def 1;
then P1: dom (((((a |^ m) |-> (a * (f . s))) | (a |^ m)) ") |^ m) = dom ((((a |^ m) |-> (a * (f . s))) | (a |^ m)) ") by FINSEQ_3:29
.= dom (((a |^ m) |-> (a * (f . s))) | (a |^ m)) by VALUED_1:def 7
.= Seg (a |^ m) ;
then J1: dom (((((a |^ m) |-> (a * (f . s))) | (a |^ m)) ") |^ m) = dom ((a |^ m) |-> ((1 / (a * (f . s))) |^ m)) ;
for k being Nat st k in dom (((((a |^ m) |-> (a * (f . s))) | (a |^ m)) ") |^ m) holds
(((((a |^ m) |-> (a * (f . s))) | (a |^ m)) ") |^ m) . k = ((a |^ m) |-> ((1 / (a * (f . s))) |^ m)) . k

proof

let k be Nat; :: thesis: ( k in dom (((((a |^ m) |-> (a * (f . s))) | (a |^ m)) ") |^ m) implies (((((a |^ m) |-> (a * (f . s))) | (a |^ m)) ") |^ m) . k = ((a |^ m) |-> ((1 / (a * (f . s))) |^ m)) . k )
assume P4: k in dom (((((a |^ m) |-> (a * (f . s))) | (a |^ m)) ") |^ m) ; :: thesis: (((((a |^ m) |-> (a * (f . s))) | (a |^ m)) ") |^ m) . k = ((a |^ m) |-> ((1 / (a * (f . s))) |^ m)) . k
then P3: k in Seg (a |^ m) by P1;
len (((((a |^ m) |-> (a * (f . s))) | (a |^ m)) ") |^ m) = len ((((a |^ m) |-> (a * (f . s))) | (a |^ m)) ") by NAT_3:def 1;
then dom (((((a |^ m) |-> (a * (f . s))) | (a |^ m)) ") |^ m) = dom ((((a |^ m) |-> (a * (f . s))) | (a |^ m)) ") by FINSEQ_3:29;
then P5: k in dom ((((a |^ m) |-> (a * (f . s))) | (a |^ m)) ") by P4;
PP: (((a |^ m) |-> (a * (f . s))) . k) " = 1 / (a * (f . s)) by P3, FUNCOP_1:7;
(((((a |^ m) |-> (a * (f . s))) | (a |^ m)) ") |^ m) . k = (((((a |^ m) |-> (a * (f . s))) | (a |^ m)) ") . k) |^ m by P4, NAT_3:def 1
.= (((((a |^ m) |-> (a * (f . s))) | (a |^ m)) . k) ") |^ m by P5, VALUED_1:def 7
.= ((a |^ m) |-> ((1 / (a * (f . s))) |^ m)) . k by PP, P3, FUNCOP_1:7 ;
hence (((((a |^ m) |-> (a * (f . s))) | (a |^ m)) ") |^ m) . k = ((a |^ m) |-> ((1 / (a * (f . s))) |^ m)) . k ; :: thesis: verum

end;

then ((((a |^ m) |-> (a * (f . s))) | (a |^ m)) ") |^ m = (a |^ m) |-> ((1 / (a * (f . s))) |^ m) by J1, FINSEQ_1:13;
then Sum (((((a |^ m) |-> (a * (f . s))) | (a |^ m)) ") |^ m) = (a to_power m) * ((1 / (a * (f . s))) to_power m) by RVSUM_1:80
.= (a / (a * (f . s))) to_power m by S1, POWER:30
.= ((a / a) / (f . s)) to_power m by XCMPLX_1:78
.= (1 / (f . s)) to_power m by XCMPLX_1:60 ;
hence Sum (((((a |^ m) |-> (a * (f . s))) | (a |^ m)) ") |^ m) = (1 / (f . s)) |^ m ; :: thesis: verum

end;

set ff = f | (s -' 1);
set gg = (a |^ m) |-> (a * (f . s));
(((f | (s -' 1)) ^ ((a |^ m) |-> (a * (f . s)))) ") |^ m = (((f | (s -' 1)) ") ^ (((a |^ m) |-> (a * (f . s))) ")) |^ m by NUMBER15:60;
then SX: (((f | (s -' 1)) ^ ((a |^ m) |-> (a * (f . s)))) ") |^ m = (((f | (s -' 1)) ") |^ m) ^ ((((a |^ m) |-> (a * (f . s))) ") |^ m) by ConcatPower;
HJ: Sum ((((a |^ m) |-> (a * (f . s))) ") |^ m) = (1 / (f . s)) |^ m by HH;
<*((f . s) ")*> = <*(f . s)*> " by NUMBER15:63;
then <*(((f . s) ") |^ m)*> = (<*(f . s)*> ") |^ m by SinglePower;
then HI: Sum ((<*(f . s)*> ") |^ m) = (1 / (f . s)) |^ m ;
Sum ((g ") |^ m) = (Sum (((f | (s -' 1)) ") |^ m)) + (Sum ((((a |^ m) |-> (a * (f . s))) ") |^ m)) by CC, SX, RVSUM_1:75
.= Sum (((f | s) ") |^ m) by K1, HI, HJ ;
hence Sum ((f ") |^ m) = Sum ((g ") |^ m) by AA; :: thesis: verum