let NT be normal NTopSpace; :: thesis: for A, B being closed Subset of NT st A misses B holds
ex F being Function of NT,FMT_R^1 st
( F is continuous & ( for x being Point of NT holds
( 0 <= F . x & F . x <= 1 & ( x in A implies F . x = 0 ) & ( x in B implies F . x = 1 ) ) ) )
let NA, NB be closed Subset of NT; :: thesis: ( NA misses NB implies ex F being Function of NT,FMT_R^1 st
( F is continuous & ( for x being Point of NT holds
( 0 <= F . x & F . x <= 1 & ( x in NA implies F . x = 0 ) & ( x in NB implies F . x = 1 ) ) ) ) )
assume A1: NA misses NB ; :: thesis: ex F being Function of NT,FMT_R^1 st
( F is continuous & ( for x being Point of NT holds
( 0 <= F . x & F . x <= 1 & ( x in NA implies F . x = 0 ) & ( x in NB implies F . x = 1 ) ) ) )
reconsider T = NTop2Top NT as non empty TopSpace ;
reconsider T = T as non empty normal TopSpace ;
reconsider A = NA, B = NB as closed Subset of T by Lm29;
consider F being Function of T,R^1 such that
A2: F is continuous and
A3: for x being Point of T holds
( 0 <= F . x & F . x <= 1 & ( x in A implies F . x = 0 ) & ( x in B implies F . x = 1 ) ) by A1, URYSOHN3:20;
reconsider TTX = T as non empty TopSpace ;
reconsider TTY = R^1 as non empty strict TopSpace ;
reconsider G = F as continuous Function of TTX,TTY by A2;
A4: ( NT = Top2NTop T & FMT_R^1 = Top2NTop R^1 ) by FINTOPO7:25;
then reconsider F9 = Top2NTop G as Function of NT,FMT_R^1 ;

now :: thesis: ( F9 is continuous & ( for x being Point of NT holds
( 0 <= F9 . x & F9 . x <= 1 & ( x in NA implies F9 . x = 0 ) & ( x in NB implies F9 . x = 1 ) ) ) )

thus F9 is continuous by A4; :: thesis: for x being Point of NT holds
( 0 <= F9 . x & F9 . x <= 1 & ( x in NA implies F9 . x = 0 ) & ( x in NB implies F9 . x = 1 ) )

now :: thesis: for x being Point of NT holds
( 0 <= F9 . x & F9 . x <= 1 )

let x be Point of NT; :: thesis: ( 0 <= F9 . x & F9 . x <= 1 )
reconsider x9 = x as Point of T by FINTOPO7:def 16;
( F9 . x = F . x & 0 <= F . x9 ) by A3;
hence 0 <= F9 . x ; :: thesis: F9 . x <= 1
( F9 . x = F . x & F . x9 <= 1 ) by A3;
hence F9 . x <= 1 ; :: thesis: verum

end;

hence for x being Point of NT holds
( 0 <= F9 . x & F9 . x <= 1 & ( x in NA implies F9 . x = 0 ) & ( x in NB implies F9 . x = 1 ) ) by A3; :: thesis: verum

end;

hence ex F being Function of NT,FMT_R^1 st
( F is continuous & ( for x being Point of NT holds
( 0 <= F . x & F . x <= 1 & ( x in NA implies F . x = 0 ) & ( x in NB implies F . x = 1 ) ) ) ) ; :: thesis: verum