let S be non empty TopSpace; :: thesis:
let T be non empty Hausdorff TopSpace; :: thesis:
let f, g be continuous Function of S,T; :: thesis:
A1: [#] T <> {} ;
thus A2: for X being Subset of S st X = { p where p is Point of S : f . p <> g . p } holds
X is open :: thesis:

proof

let X be Subset of S; :: thesis:
assume A3: X = { p where p is Point of S : f . p <> g . p } ; :: thesis:
for x being set holds
( x in X iff ex Q being Subset of S st
( Q is open & Q c= X & x in Q ) )

proof

let x be set ; :: thesis:

hereby :: thesis:

assume x in X ; :: thesis:
then consider p being Point of S such that
A4: ( x = p & f . p <> g . p ) by A3;
consider W, V being Subset of T such that
A5: ( W is open & V is open ) and
A6: ( f . p in W & g . p in V ) and
A7: W misses V by A4, PRE_TOPC:def 16;
take Q = (f " W) /\ (g " V); :: thesis:
( f " W is open & g " V is open ) by A1, A5, TOPS_2:55;
hence Q is open by TOPS_1:38; :: thesis:
thus Q c= X :: thesis:

proof

let q be set ; :: according to TARSKI:def 3 :: thesis:
assume A8: q in Q ; :: thesis:
then q in f " W by XBOOLE_0:def 4;
then consider yf being set such that
A9: ( [q,yf] in f & yf in W ) by RELAT_1:def 14;
q in g " V by A8, XBOOLE_0:def 4;
then consider yg being set such that
A10: ( [q,yg] in g & yg in V ) by RELAT_1:def 14;
A11: ( yf = f . q & yg = g . q ) by A9, A10, FUNCT_1:8;
not yg in W by A7, A10, XBOOLE_0:3;
hence q in X by A3, A8, A9, A11; :: thesis:

end;

dom f = the carrier of S by FUNCT_2:def 1;
then [x,(f . p)] in f by A4, FUNCT_1:def 4;
then A12: x in f " W by A6, RELAT_1:def 14;
dom g = the carrier of S by FUNCT_2:def 1;
then [x,(g . p)] in g by A4, FUNCT_1:def 4;
then x in g " V by A6, RELAT_1:def 14;
hence x in Q by A12, XBOOLE_0:def 4; :: thesis:

end;

given Q being Subset of S such that A13: ( Q is open & Q c= X & x in Q ) ; :: thesis:
thus x in X by A13; :: thesis:

end;

hence X is open by TOPS_1:57; :: thesis:

end;

let X be Subset of S; :: thesis:
assume A14: X = { p where p is Point of S : f . p = g . p } ; :: thesis:
{ p where p is Point of S : f . p <> g . p } c= the carrier of S

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in { p where p is Point of S : f . p <> g . p } ; :: thesis:
then consider a being Point of S such that
A15: ( x = a & f . a <> g . a ) ;
thus x in the carrier of S by A15; :: thesis:

end;

then reconsider A = { p where p is Point of S : f . p <> g . p } as Subset of S ;
A16: X ` = A

proof

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis:

let x be set ; :: thesis:
assume A17: x in X ` ; :: thesis:
then not x in X by XBOOLE_0:def 5;
then f . x <> g . x by A14, A17;
hence x in A by A17; :: thesis:

end;

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in A ; :: thesis:
then consider p being Point of S such that
A18: ( x = p & f . p <> g . p ) ;

now

assume p in { t where t is Point of S : f . t = g . t } ; :: thesis:
then consider t being Point of S such that
A19: ( p = t & f . t = g . t ) ;
thus contradiction by A18, A19; :: thesis:

end;

hence x in X ` by A14, A18, XBOOLE_0:def 5; :: thesis:

end;

A is open by A2;
hence X is closed by A16, TOPS_1:29; :: thesis: