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 set ; :: 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 set such that
A1: z in dom (f ~ ) and
A2: [x,y] = (f ~ ) . z by FUNCT_1:def 5;
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 5;
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 set such that
A4: ( z in dom f & [y,x] = f . z ) by FUNCT_1:def 5;
( z in dom (f ~ ) & (f ~ ) . z = [x,y] ) by A4, Def1;
hence [x,y] in rng (f ~ ) by FUNCT_1:def 5; :: thesis: verum