let f be Function; :: thesis: for x, z being object st x in dom f & z in rng (renameElementsDistinctlyFunc (f,x)) holds
ex y being object st
( y in f . x & z = [f,x,y] )
let x, z be object ; :: thesis: ( x in dom f & z in rng (renameElementsDistinctlyFunc (f,x)) implies ex y being object st
( y in f . x & z = [f,x,y] ) )
assume A1: ( x in dom f & z in rng (renameElementsDistinctlyFunc (f,x)) ) ; :: thesis: ex y being object st
( y in f . x & z = [f,x,y] )
then consider y being object such that
A2: y in dom (renameElementsDistinctlyFunc (f,x)) and
A3: (renameElementsDistinctlyFunc (f,x)) . y = z by FUNCT_1:def 3;
take y ; :: thesis: ( y in f . x & z = [f,x,y] )
thus y in f . x by A2; :: thesis: z = [f,x,y]
hence z = [f,x,y] by A1, A3, Th78; :: thesis: verum