let IT, IT9 be Function of R,(bool R); :: thesis: ( ( 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} ; :: thesis: IT = IT9

now :: thesis: for x being Element of R holds IT . x = IT9 . x

let x be Element of R; :: thesis: IT . x = IT9 . x
IT . x = {x} by A3;
hence IT . x = IT9 . x by A4; :: thesis: verum

end;

hence IT = IT9 ; :: thesis: verum