A1: X = dom f by FUNCT_2:def 1
.= dom (f ~ ) by Def1 ;
rng (f ~ ) c= [:Z,Y:]

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (f ~ ) or x in [:Z,Y:] )
assume x in rng (f ~ ) ; :: thesis: x in [:Z,Y:]
then consider y being set such that
A2: y in dom (f ~ ) and
A3: x = (f ~ ) . y by FUNCT_1:def 5;
A4: y in dom f by A2, Def1;
then reconsider y = y as Element of X ;
A5: f . y = [((f . y) `1 ),((f . y) `2 )] by MCART_1:23;
then (f ~ ) . y = [((f . y) `2 ),((f . y) `1 )] by A4, Def1;
hence x in [:Z,Y:] by A3, A5, ZFMISC_1:107; :: thesis: verum

end;

hence f ~ is Function of X,[:Z,Y:] by A1, FUNCT_2:def 1, RELSET_1:11; :: thesis: verum