A1: rng (f ~) c= [:Z,Y:]

proof

let x be object ; :: 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 object such that
A2: y in dom (f ~) and
A3: x = (f ~) . y by FUNCT_1:def 3;
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:21;
then (f ~) . y = [((f . y) `2),((f . y) `1)] by A4, Def1;
hence x in [:Z,Y:] by A3, A5, ZFMISC_1:88; :: thesis: verum

end;

X = dom f by FUNCT_2:def 1
.= dom (f ~) by Def1 ;
hence f ~ is Function of X,[:Z,Y:] by A1, FUNCT_2:def 1, RELSET_1:4; :: thesis: verum