let X, Y, Z be non empty set ; :: thesis: for f being Function of X,[:Y,Z:] holds rng (f ~) = (rng f) ~
let f be Function of X,[:Y,Z:]; :: thesis: rng (f ~) = (rng f) ~
let x, y be object ; :: according to RELAT_1:def 2 :: thesis: ( ( not [x,y] in rng (f ~) or [x,y] in (rng f) ~ ) & ( not [x,y] in (rng f) ~ or [x,y] in rng (f ~) ) )
thus ( [x,y] in rng (f ~) implies [x,y] in (rng f) ~ ) :: thesis: ( not [x,y] in (rng f) ~ or [x,y] in rng (f ~) )

proof

assume [x,y] in rng (f ~) ; :: thesis: [x,y] in (rng f) ~
then consider z being object such that
A1: z in dom (f ~) and
A2: [x,y] = (f ~) . z by FUNCT_1:def 3;
A3: z in dom f by A1, Def1;
f . z = ((f ~) ~) . z
.= [y,x] by A1, A2, Def1 ;
then [y,x] in rng f by A3, FUNCT_1:def 3;
hence [x,y] in (rng f) ~ by RELAT_1:def 7; :: thesis: verum

end;

assume [x,y] in (rng f) ~ ; :: thesis: [x,y] in rng (f ~)
then [y,x] in rng f by RELAT_1:def 7;
then consider z being object such that
A4: ( z in dom f & [y,x] = f . z ) by FUNCT_1:def 3;
( z in dom (f ~) & (f ~) . z = [x,y] ) by A4, Def1;
hence [x,y] in rng (f ~) by FUNCT_1:def 3; :: thesis: verum