let A be FinSequence; :: thesis: for a being set holds
( ( A <> {} & #occurrences (a,A) = len A ) iff a in meet (rng A) )
let a be set ; :: thesis: ( ( A <> {} & #occurrences (a,A) = len A ) iff a in meet (rng A) )
A1: { 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;

A2: ( dom A = Seg (len A) & card (Seg (len A)) = len A ) by FINSEQ_1:57, FINSEQ_1:def 3;

hereby :: thesis: ( a in meet (rng A) implies ( A <> {} & #occurrences (a,A) = len A ) )

assume A <> {} ; :: thesis: ( #occurrences (a,A) = len A implies a in meet (rng A) )
then A3: rng A <> {} by RELAT_1:41;
assume A4: #occurrences (a,A) = len A ; :: thesis: a in meet (rng A)
A5: { i where i is Element of NAT : ( i in dom A & a in A . i ) } = dom A by A4, A1, A2, CARD_2:102;

now :: thesis: for z being set st z in rng A holds
a in z

let z be set ; :: thesis: ( z in rng A implies a in z )
assume z in rng A ; :: thesis: a in z
then consider s being object such that
A6: ( s in dom A & z = A . s ) by FUNCT_1:def 3;
consider i being Element of NAT such that
A7: ( s = i & i in dom A & a in A . i ) by A5, A6;
thus a in z by A6, A7; :: thesis: verum

end;

hence a in meet (rng A) by A3, SETFAM_1:def 1; :: thesis: verum

end;

assume A8: a in meet (rng A) ; :: thesis: ( A <> {} & #occurrences (a,A) = len A )
thus A <> {} by A8, RELAT_1:38, SETFAM_1:def 1; :: thesis: #occurrences (a,A) = len A
dom A c= { i where i is Element of NAT : ( i in dom A & a in A . i ) }

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in dom A or z in { i where i is Element of NAT : ( i in dom A & a in A . i ) } )
assume A9: z in dom A ; :: thesis: z in { i where i is Element of NAT : ( i in dom A & a in A . i ) }
then A . z in rng A by FUNCT_1:def 3;
then a in A . z by A8, SETFAM_1:def 1;
hence z in { i where i is Element of NAT : ( i in dom A & a in A . i ) } by A9; :: thesis: verum

end;

hence #occurrences (a,A) = len A by A2, A1, XBOOLE_0:def 10; :: thesis: verum