let x be object ; :: 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 object 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