let i, n be Nat; :: thesis: for f being FinSequence holds count_reps ((f ^ <*(i + 1)*>),n) = (count_reps (f,n)) + ((EmptyBag n) +* (i,1))
let f be FinSequence; :: thesis: count_reps ((f ^ <*(i + 1)*>),n) = (count_reps (f,n)) + ((EmptyBag n) +* (i,1))
set s1 = count_reps ((f ^ <*(i + 1)*>),n);
set s = count_reps (f,n);
set E = EmptyBag n;
A1: ( dom (count_reps ((f ^ <*(i + 1)*>),n)) = n & n = dom ((count_reps (f,n)) + ((EmptyBag n) +* (i,1))) & n = dom (EmptyBag n) ) by PARTFUN1:def 2;
for x being object st x in dom (count_reps ((f ^ <*(i + 1)*>),n)) holds
(count_reps ((f ^ <*(i + 1)*>),n)) . x = ((count_reps (f,n)) + ((EmptyBag n) +* (i,1))) . x

proof

let x be object ; :: thesis: ( x in dom (count_reps ((f ^ <*(i + 1)*>),n)) implies (count_reps ((f ^ <*(i + 1)*>),n)) . x = ((count_reps (f,n)) + ((EmptyBag n) +* (i,1))) . x )
assume A2: x in dom (count_reps ((f ^ <*(i + 1)*>),n)) ; :: thesis: (count_reps ((f ^ <*(i + 1)*>),n)) . x = ((count_reps (f,n)) + ((EmptyBag n) +* (i,1))) . x
x in Segm n by A2;
then reconsider a = x as Nat ;
A3: card ((f ^ <*(i + 1)*>) " {(a + 1)}) = (card (f " {(a + 1)})) + (card (<*(i + 1)*> " {(a + 1)})) by FINSEQ_3:57;
A4: rng <*(i + 1)*> = {(i + 1)} by FINSEQ_1:38;

per cases ( a <> i or a = i ) ;

suppose A5: a <> i ; :: thesis: (count_reps ((f ^ <*(i + 1)*>),n)) . x = ((count_reps (f,n)) + ((EmptyBag n) +* (i,1))) . x

then a + 1 <> i + 1 ;
then A6: <*(i + 1)*> " {(a + 1)} = {} by A4, RELAT_1:138, ZFMISC_1:11;
A7: ( ((EmptyBag n) +* (i,1)) . a = (EmptyBag n) . a & (EmptyBag n) . a = 0 ) by A5, FUNCT_7:32;
thus (count_reps ((f ^ <*(i + 1)*>),n)) . x = (card (f " {(a + 1)})) + 0 by A6, A2, Def8, A3
.= ((count_reps (f,n)) . a) + 0 by A2, Def8
.= ((count_reps (f,n)) + ((EmptyBag n) +* (i,1))) . x by A7, A2, A1, VALUED_1:def 1 ; :: thesis: verum

end;

suppose A8: a = i ; :: thesis: (count_reps ((f ^ <*(i + 1)*>),n)) . x = ((count_reps (f,n)) + ((EmptyBag n) +* (i,1))) . x

then A9: ( <*(i + 1)*> " {(a + 1)} = dom <*(i + 1)*> & dom <*(i + 1)*> = Seg 1 & Seg 1 = {1} ) by A4, RELAT_1:134, FINSEQ_1:38, FINSEQ_1:2;
A10: ((EmptyBag n) +* (i,1)) . a = 1 by A8, A1, A2, FUNCT_7:31;
thus (count_reps ((f ^ <*(i + 1)*>),n)) . x = (card (f " {(a + 1)})) + 1 by A9, A2, Def8, A3
.= ((count_reps (f,n)) . a) + 1 by A2, Def8
.= ((count_reps (f,n)) + ((EmptyBag n) +* (i,1))) . x by A10, A2, A1, VALUED_1:def 1 ; :: thesis: verum

end;

end;

end;

hence count_reps ((f ^ <*(i + 1)*>),n) = (count_reps (f,n)) + ((EmptyBag n) +* (i,1)) by A1; :: thesis: verum