let f be Function; :: thesis: for x, y being object st x in dom f & y in f . x holds
(renameElementsDistinctlyFunc (f,x)) . y = [f,x,y]
let x, y be object ; :: thesis: ( x in dom f & y in f . x implies (renameElementsDistinctlyFunc (f,x)) . y = [f,x,y] )
assume A1: ( x in dom f & y in f . x ) ; :: thesis: (renameElementsDistinctlyFunc (f,x)) . y = [f,x,y]
then y in dom (renameElementsDistinctlyFunc (f,x)) by PARTFUN1:def 2;
hence (renameElementsDistinctlyFunc (f,x)) . y = [(((f . x) --> [f,x]) . y),((id (f . x)) . y)] by FUNCT_3:def 7
.= [[f,x],((id (f . x)) . y)] by A1, FUNCOP_1:7
.= [[f,x],y] by A1, FUNCT_1:18
.= [f,x,y] by XTUPLE_0:def 4 ;
:: thesis: verum