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 ;
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 ;
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 ; :: thesis: verum
end;
assume A8: a in meet (rng A) ; :: thesis: ( A <> {} & #occurrences (a,A) = len A )
thus A <> {} by ; :: 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 ;
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 ; :: thesis: verum