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

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 ) }

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

A2:
( dom A = Seg (len A) & card (Seg (len A)) = len A )
by 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

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

assume A8:
a in meet (rng A)
; :: thesis: ( 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;

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

hence
a in meet (rng A)
by A3, SETFAM_1:def 1; :: thesis: veruma 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;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

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

hence
#occurrences (a,A) = len A
by A2, A1, XBOOLE_0:def 10; :: thesis: verum
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;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