let n be Nat; :: thesis: for f being FinSequence of Seg n
for i being Nat st i in n & count_reps (f,n) = (EmptyBag n) +* (i,(len f)) holds
f = (len f) |-> (i + 1)
set E = EmptyBag n;
let f be FinSequence of Seg n; :: thesis: for i being Nat st i in n & count_reps (f,n) = (EmptyBag n) +* (i,(len f)) holds
f = (len f) |-> (i + 1)
let i be Nat; :: thesis: ( i in n & count_reps (f,n) = (EmptyBag n) +* (i,(len f)) implies f = (len f) |-> (i + 1) )
assume A1: ( i in n & count_reps (f,n) = (EmptyBag n) +* (i,(len f)) ) ; :: thesis: f = (len f) |-> (i + 1)
dom (EmptyBag n) = n by PARTFUN1:def 2;
then (count_reps (f,n)) . i = len f by A1, FUNCT_7:31;
then A2: len f = card (f " {(i + 1)}) by Def8, A1;
A3: dom f = Seg (len f) by FINSEQ_1:def 3;
then card (dom f) = len f ;
then A4: dom f = f " {(i + 1)} by A2, RELAT_1:132, CARD_2:102;
for x being object st x in dom f holds
f . x = i + 1

proof

let x be object ; :: thesis: ( x in dom f implies f . x = i + 1 )
assume x in dom f ; :: thesis: f . x = i + 1
then f . x in {(i + 1)} by A4, FUNCT_1:def 7;
hence f . x = i + 1 by TARSKI:def 1; :: thesis: verum

end;

hence f = (len f) |-> (i + 1) by A3, FUNCOP_1:11; :: thesis: verum