let f be Function; :: thesis: ( proj1 (dom f) = proj2 (dom (~ f)) & proj2 (dom f) = proj1 (dom (~ f)) )
thus proj1 (dom f) c= proj2 (dom (~ f)) :: according to XBOOLE_0:def 10 :: thesis: ( proj2 (dom (~ f)) c= proj1 (dom f) & proj2 (dom f) = proj1 (dom (~ f)) )

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in proj1 (dom f) or x in proj2 (dom (~ f)) )
assume x in proj1 (dom f) ; :: thesis: x in proj2 (dom (~ f))
then consider y being object such that
A1: [x,y] in dom f by XTUPLE_0:def 12;
[y,x] in dom (~ f) by A1, FUNCT_4:42;
hence x in proj2 (dom (~ f)) by XTUPLE_0:def 13; :: thesis: verum

end;

thus proj2 (dom (~ f)) c= proj1 (dom f) :: thesis: proj2 (dom f) = proj1 (dom (~ f))

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in proj2 (dom (~ f)) or y in proj1 (dom f) )
assume y in proj2 (dom (~ f)) ; :: thesis: y in proj1 (dom f)
then consider x being object such that
A2: [x,y] in dom (~ f) by XTUPLE_0:def 13;
[y,x] in dom f by A2, FUNCT_4:42;
hence y in proj1 (dom f) by XTUPLE_0:def 12; :: thesis: verum

end;

thus proj2 (dom f) c= proj1 (dom (~ f)) :: according to XBOOLE_0:def 10 :: thesis: proj1 (dom (~ f)) c= proj2 (dom f)

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in proj2 (dom f) or y in proj1 (dom (~ f)) )
assume y in proj2 (dom f) ; :: thesis: y in proj1 (dom (~ f))
then consider x being object such that
A3: [x,y] in dom f by XTUPLE_0:def 13;
[y,x] in dom (~ f) by A3, FUNCT_4:42;
hence y in proj1 (dom (~ f)) by XTUPLE_0:def 12; :: thesis: verum

end;

thus proj1 (dom (~ f)) c= proj2 (dom f) :: thesis: verum

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in proj1 (dom (~ f)) or x in proj2 (dom f) )
assume x in proj1 (dom (~ f)) ; :: thesis: x in proj2 (dom f)
then consider y being object such that
A4: [x,y] in dom (~ f) by XTUPLE_0:def 12;
[y,x] in dom f by A4, FUNCT_4:42;
hence x in proj2 (dom f) by XTUPLE_0:def 13; :: thesis: verum

end;