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

hence #occurrences (a,A) <= len A by NAT_1:39; :: thesis: verum

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

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;
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;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

hence #occurrences (a,A) <= len A by NAT_1:39; :: thesis: verum