let A be FinSequence; :: thesis: for a being set holds #occurrences (a,A) <= len A
let a be set ; :: thesis: #occurrences (a,A) <= len A
{ i where i is Element of NAT : ( i in dom A & a in A . i ) } c= dom A

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in { i where i is Element of NAT : ( i in dom A & a in A . i ) } or z in dom A )
assume z in { i where i is Element of NAT : ( i in dom A & a in A . i ) } ; :: thesis: z in dom A
then ex i being Element of NAT st
( z = i & i in dom A & a in A . i ) ;
hence z in dom A ; :: thesis: verum

end;

then ( Segm (#occurrences (a,A)) c= Segm (card (dom A)) & dom A = Seg (len A) & card (Seg (len A)) = len A ) by CARD_1:11, FINSEQ_1:57, FINSEQ_1:def 3;
hence #occurrences (a,A) <= len A by NAT_1:39; :: thesis: verum