{ i where i is Element of NAT : ( i in dom A & a in A . i ) } c= dom A

proof

hence
card { i where i is Element of NAT : ( i in dom A & a in A . i ) } is Nat
; :: thesis: verum
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