let X1, X2 be set ; ( ( for x being set holds
( x in X1 iff ex y being finite set ex z being set st
( x = [y,z] & y in dom f & z in f . y ) ) ) & ( for x being set holds
( x in X2 iff ex y being finite set ex z being set st
( x = [y,z] & y in dom f & z in f . y ) ) ) implies X1 = X2 )
assume A5:
( ( for x being set holds
( x in X1 iff ex y being finite set ex z being set st
( x = [y,z] & y in dom f & z in f . y ) ) ) & ( for x being set holds
( x in X2 iff ex y being finite set ex z being set st
( x = [y,z] & y in dom f & z in f . y ) ) ) & not X1 = X2 )
; contradiction
then consider x being object such that
A6:
( ( x in X1 & not x in X2 ) or ( x in X2 & not x in X1 ) )
by TARSKI:2;
( x in X2 iff for y being finite set
for z being set holds
( not x = [y,z] or not y in dom f or not z in f . y ) )
by A5, A6;
hence
contradiction
by A5; verum