let A, B be set ; :: thesis: ( ( for x being object holds ( x in A iff f . x <>0 ) ) & ( for x being object holds ( x in B iff f . x <>0 ) ) implies A = B ) assume that A3:
for x being object holds ( x in A iff f . x <>0 )
and A4:
for x being object holds ( x in B iff f . x <>0 )
; :: thesis: A = B
for x being object holds ( x in A iff x in B )