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

end;

let z be set ; :: thesis:
assume z in rng A ; :: thesis:
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:

end;

end;

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

let z be object ; :: according to TARSKI:def 3 :: thesis:
assume A9: z in dom A ; :: thesis:
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:

end;