let f be Function; :: thesis:
let x be object ; :: thesis:

per cases ;

suppose A1: x in dom f ; :: thesis:

now :: thesis:

let z be object ; :: thesis:

hereby :: thesis:

assume z in rng (renameElementsDistinctlyFunc (f,x)) ; :: thesis:
then consider y being object such that
A2: ( y in f . x & z = [f,x,y] ) by A1, Th79;
A3: [f,x] in {[f,x]} by TARSKI:def 1;
z = [[f,x],y] by A2, XTUPLE_0:def 4;
hence z in [:{[f,x]},(f . x):] by A2, A3, ZFMISC_1:def 2; :: thesis:

end;

assume z in [:{[f,x]},(f . x):] ; :: thesis:
then consider z1, y being object such that
A4: ( z1 in {[f,x]} & y in f . x & z = [z1,y] ) by ZFMISC_1:def 2;
z1 = [f,x] by A4, TARSKI:def 1;
then A5: z = [f,x,y] by A4, XTUPLE_0:def 4;
y in dom (renameElementsDistinctlyFunc (f,x)) by A4, PARTFUN1:def 2;
then (renameElementsDistinctlyFunc (f,x)) . y in rng (renameElementsDistinctlyFunc (f,x)) by FUNCT_1:3;
hence z in rng (renameElementsDistinctlyFunc (f,x)) by A1, A4, A5, Th78; :: thesis:

end;

hence rng (renameElementsDistinctlyFunc (f,x)) = [:{[f,x]},(f . x):] by TARSKI:2; :: thesis:

end;

suppose not x in dom f ; :: thesis:

then f . x = {} by FUNCT_1:def 2;
then A6: ( dom (renameElementsDistinctlyFunc (f,x)) = {} & [:{[f,x]},(f . x):] = {} ) by ZFMISC_1:90;
then renameElementsDistinctlyFunc (f,x) = {} ;
hence rng (renameElementsDistinctlyFunc (f,x)) = [:{[f,x]},(f . x):] by A6; :: thesis:

end;

end;