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

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