let i, n, m be Nat; :: thesis: ( i in n implies count_reps ((m |-> (i + 1)),n) = (EmptyBag n) +* (i,m) )
set E = EmptyBag n;
set s = count_reps ((m |-> (i + 1)),n);
assume i in n ; :: thesis: count_reps ((m |-> (i + 1)),n) = (EmptyBag n) +* (i,m)
A1: ( dom (count_reps ((m |-> (i + 1)),n)) = n & n = dom ((EmptyBag n) +* (i,m)) & n = dom (EmptyBag n) ) by PARTFUN1:def 2;
for x being object st x in n holds
(count_reps ((m |-> (i + 1)),n)) . x = ((EmptyBag n) +* (i,m)) . x

proof

let x be object ; :: thesis: ( x in n implies (count_reps ((m |-> (i + 1)),n)) . x = ((EmptyBag n) +* (i,m)) . x )
assume A2: x in n ; :: thesis: (count_reps ((m |-> (i + 1)),n)) . x = ((EmptyBag n) +* (i,m)) . x
then x in Segm n ;
then reconsider a = x as Nat ;
A3: (count_reps ((m |-> (i + 1)),n)) . a = card ((m |-> (i + 1)) " {(a + 1)}) by A2, Def8;

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

suppose A4: a = i ; :: thesis: (count_reps ((m |-> (i + 1)),n)) . x = ((EmptyBag n) +* (i,m)) . x

((Seg m) --> (i + 1)) " {(a + 1)} = Seg m by A4, FUNCOP_1:15;
hence (count_reps ((m |-> (i + 1)),n)) . x = ((EmptyBag n) +* (i,m)) . x by A3, A4, A1, A2, FUNCT_7:31; :: thesis: verum

end;

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

then A6: ((EmptyBag n) +* (i,m)) . x = (EmptyBag n) . x by FUNCT_7:32;
a + 1 <> i + 1 by A5;
then not i + 1 in {(a + 1)} by TARSKI:def 1;
then ((Seg m) --> (i + 1)) " {(a + 1)} = {} by FUNCOP_1:16;
hence (count_reps ((m |-> (i + 1)),n)) . x = ((EmptyBag n) +* (i,m)) . x by A6, A3; :: thesis: verum

end;

end;

end;

hence count_reps ((m |-> (i + 1)),n) = (EmptyBag n) +* (i,m) by A1; :: thesis: verum