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

.= dom (f ~) by Def1 ;

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

proof

X =
dom f
by FUNCT_2:def 1
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;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

.= dom (f ~) by Def1 ;

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