let X, Y be set ; :: thesis: for f being Function st dom f = [:X,Y:] holds
dom (~ f) = [:Y,X:]
let f be Function; :: thesis: ( dom f = [:X,Y:] implies dom (~ f) = [:Y,X:] )
assume A1: dom f = [:X,Y:] ; :: thesis: dom (~ f) = [:Y,X:]
hence dom (~ f) c= [:Y,X:] by Th45; :: according to XBOOLE_0:def 10 :: thesis: [:Y,X:] c= dom (~ f)
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in [:Y,X:] or z in dom (~ f) )
assume z in [:Y,X:] ; :: thesis: z in dom (~ f)
then consider y, x being object such that
A2: ( y in Y & x in X ) and
A3: z = [y,x] by ZFMISC_1:def 2;
[x,y] in dom f by A1, A2, ZFMISC_1:def 2;
hence z in dom (~ f) by A3, Def2; :: thesis: verum