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

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

hence
IT = IT9
; :: thesis: verumlet 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;IT . x = {x} by A3;

hence IT . x = IT9 . x by A4; :: thesis: verum