let IT, IT9 be Function of R,(bool R); ( ( for x being Element of R holds IT . x = {x} ) & ( for x being Element of R holds IT9 . x = {x} ) implies IT = IT9 )
assume that
A3:
for x being Element of R holds IT . x = {x}
and
A4:
for x being Element of R holds IT9 . x = {x}
; IT = IT9
hence
IT = IT9
; verum