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 ~) )

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

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 ~)
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;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

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