let f be Function; :: thesis: for x1, x2 being object holds rng (renameElementsDistinctlyFunc (f,x1)) misses f . x2
let x1, x2 be object ; :: thesis: rng (renameElementsDistinctlyFunc (f,x1)) misses f . x2

per cases ( ( x1 in dom f & x2 in dom f ) or not x1 in dom f or not x2 in dom f ) ;

suppose A1: ( x1 in dom f & x2 in dom f ) ; :: thesis: rng (renameElementsDistinctlyFunc (f,x1)) misses f . x2

(rng (renameElementsDistinctlyFunc (f,x1))) /\ (f . x2) = {}

proof

assume (rng (renameElementsDistinctlyFunc (f,x1))) /\ (f . x2) <> {} ; :: thesis: contradiction
then consider z being object such that
A2: z in (rng (renameElementsDistinctlyFunc (f,x1))) /\ (f . x2) by XBOOLE_0:def 1;
A3: z in rng (renameElementsDistinctlyFunc (f,x1)) by A2, XBOOLE_0:def 4;
consider y being object such that
A4: ( y in f . x1 & z = [f,x1,y] ) by A1, A3, Th79;
reconsider X1 = z, X4 = [x2,(f . x2)], X7 = [f,x1], X9 = [[f,x1],y] as set by TARSKI:1;
A5: z in f . x2 by A2, XBOOLE_0:def 4;
A6: f . x2 in {x2,(f . x2)} by TARSKI:def 2;
{x2,(f . x2)} in {{x2,(f . x2)},{x2}} by TARSKI:def 2;
then A7: {x2,(f . x2)} in X4 by TARSKI:def 5;
A8: [x2,(f . x2)] in f by A1, FUNCT_1:1;
A9: f in {f} by TARSKI:def 1;
{f} in {{f,x1},{f}} by TARSKI:def 2;
then A10: {f} in X7 by TARSKI:def 5;
A11: [f,x1] in {[f,x1]} by TARSKI:def 1;
{[f,x1]} in {{[f,x1],y},{[f,x1]}} by TARSKI:def 2;
then {[f,x1]} in X9 by TARSKI:def 5;
then {[f,x1]} in X1 by A4, XTUPLE_0:def 4;
hence contradiction by A5, A6, A7, A8, A9, A10, A11, GLIBPRE1:2; :: thesis: verum

end;

hence rng (renameElementsDistinctlyFunc (f,x1)) misses f . x2 by XBOOLE_0:def 7; :: thesis: verum

end;

suppose not x1 in dom f ; :: thesis: rng (renameElementsDistinctlyFunc (f,x1)) misses f . x2

then f . x1 = {} by FUNCT_1:def 2;
then {} = rng (renameElementsDistinctlyFunc (f,x1)) ;
hence rng (renameElementsDistinctlyFunc (f,x1)) misses f . x2 by XBOOLE_1:65; :: thesis: verum

end;

suppose not x2 in dom f ; :: thesis: rng (renameElementsDistinctlyFunc (f,x1)) misses f . x2

then f . x2 = {} by FUNCT_1:def 2;
hence rng (renameElementsDistinctlyFunc (f,x1)) misses f . x2 by XBOOLE_1:65; :: thesis: verum

end;

end;