let n be Nat; :: thesis: for f being FinSequence of Seg n holds degree (count_reps (f,n)) = len f
defpred S₁[ Nat] means for f being FinSequence of Seg n st len f = $1 holds
degree (count_reps (f,n)) = len f;
A1: S₁[ 0 ]

proof

let f be FinSequence of Seg n; :: thesis: ( len f = 0 implies degree (count_reps (f,n)) = len f )
assume A2: len f = 0 ; :: thesis: degree (count_reps (f,n)) = len f
f = {} by A2;
then count_reps (f,n) = EmptyBag n by Th54;
hence degree (count_reps (f,n)) = len f by UPROOTS:11, A2; :: thesis: verum

end;

A3: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A4: S₁[i] ; :: thesis: S₁[i + 1]
let f be FinSequence of Seg n; :: thesis: ( len f = i + 1 implies degree (count_reps (f,n)) = len f )
assume A5: len f = i + 1 ; :: thesis: degree (count_reps (f,n)) = len f
1 <= i + 1 by NAT_1:11;
then i + 1 in dom f by A5, FINSEQ_3:25;
then A6: ( f . (i + 1) in rng f & rng f c= Seg n ) by FUNCT_1:def 3, FINSEQ_1:def 4;
then f . (i + 1) >= 1 by FINSEQ_1:1;
then reconsider fi1 = (f . (i + 1)) - 1 as Nat ;
set fi = f | i;
set F = <*(fi1 + 1)*>;
A7: len (f | i) = i by NAT_1:11, A5, FINSEQ_1:59;
then A8: degree (count_reps ((f | i),n)) = len (f | i) by A4;
fi1 + 1 <= n by A6, FINSEQ_1:1;
then fi1 < n by NAT_1:13;
then A9: fi1 in Segm n by NAT_1:44;
reconsider N = n as non empty set by A5;
reconsider a = fi1 as Element of N by A9;
reconsider A = {fi1} as Subset of N by A9, ZFMISC_1:31;
(EmptyBag n) +* (fi1,1) = ({a},1) -bag by Th12;
then A10: ( degree ((EmptyBag n) +* (fi1,1)) = card {a} & card {a} = 1 ) by UPROOTS:13, CARD_1:30;
f = (f | i) ^ <*(fi1 + 1)*> by FINSEQ_3:55, A5;
then count_reps (f,n) = (count_reps ((f | i),n)) + ((EmptyBag n) +* (fi1,1)) by Th55;
hence degree (count_reps (f,n)) = len f by A10, A8, A7, A5, UPROOTS:15; :: thesis: verum

end;

for i being Nat holds S₁[i] from NAT_1:sch 2(A1, A3);
hence for f being FinSequence of Seg n holds degree (count_reps (f,n)) = len f ; :: thesis: verum