let x be set ; :: according to FUNCOP_1:def 6 :: thesis: ( not x in dom (~ f) or (~ f) . x is set )
assume x in dom (~ f) ; :: thesis: (~ f) . x is set
then consider z, y being set such that
A1: x = [y,z] and
A2: [z,y] in dom f by FUNCT_4:def 2;
f . z,y = (~ f) . y,z by A2, FUNCT_4:def 2;
hence (~ f) . x is set by A1; :: thesis: verum