let U be Subset of Niemytzki-plane ; :: thesis: for x being Element of REAL
for r being real positive number st U = (Ball |[x,r]|,r) \/ {|[x,0 ]|} holds
ex f being continuous Function of Niemytzki-plane ,I[01] st
( f . |[x,0 ]| = 0 & ( for a, b being real number holds
( ( |[a,b]| in U ` implies f . |[a,b]| = 1 ) & ( |[a,b]| in U \ {|[x,0 ]|} implies f . |[a,b]| = (|.(|[x,0 ]| - |[a,b]|).| ^2 ) / ((2 * r) * b) ) ) ) )
let x be Element of REAL ; :: thesis: for r being real positive number st U = (Ball |[x,r]|,r) \/ {|[x,0 ]|} holds
ex f being continuous Function of Niemytzki-plane ,I[01] st
( f . |[x,0 ]| = 0 & ( for a, b being real number holds
( ( |[a,b]| in U ` implies f . |[a,b]| = 1 ) & ( |[a,b]| in U \ {|[x,0 ]|} implies f . |[a,b]| = (|.(|[x,0 ]| - |[a,b]|).| ^2 ) / ((2 * r) * b) ) ) ) )
let r be real positive number ; :: thesis: ( U = (Ball |[x,r]|,r) \/ {|[x,0 ]|} implies ex f being continuous Function of Niemytzki-plane ,I[01] st
( f . |[x,0 ]| = 0 & ( for a, b being real number holds
( ( |[a,b]| in U ` implies f . |[a,b]| = 1 ) & ( |[a,b]| in U \ {|[x,0 ]|} implies f . |[a,b]| = (|.(|[x,0 ]| - |[a,b]|).| ^2 ) / ((2 * r) * b) ) ) ) ) )
assume A1: U = (Ball |[x,r]|,r) \/ {|[x,0 ]|} ; :: thesis: ex f being continuous Function of Niemytzki-plane ,I[01] st
( f . |[x,0 ]| = 0 & ( for a, b being real number holds
( ( |[a,b]| in U ` implies f . |[a,b]| = 1 ) & ( |[a,b]| in U \ {|[x,0 ]|} implies f . |[a,b]| = (|.(|[x,0 ]| - |[a,b]|).| ^2 ) / ((2 * r) * b) ) ) ) )
take f = + x,r; :: thesis: ( f . |[x,0 ]| = 0 & ( for a, b being real number holds
( ( |[a,b]| in U ` implies f . |[a,b]| = 1 ) & ( |[a,b]| in U \ {|[x,0 ]|} implies f . |[a,b]| = (|.(|[x,0 ]| - |[a,b]|).| ^2 ) / ((2 * r) * b) ) ) ) )
thus f . |[x,0 ]| = 0 by Def5; :: thesis: for a, b being real number holds
( ( |[a,b]| in U ` implies f . |[a,b]| = 1 ) & ( |[a,b]| in U \ {|[x,0 ]|} implies f . |[a,b]| = (|.(|[x,0 ]| - |[a,b]|).| ^2 ) / ((2 * r) * b) ) )
let a, b be real number ; :: thesis: ( ( |[a,b]| in U ` implies f . |[a,b]| = 1 ) & ( |[a,b]| in U \ {|[x,0 ]|} implies f . |[a,b]| = (|.(|[x,0 ]| - |[a,b]|).| ^2 ) / ((2 * r) * b) ) )
thus ( |[a,b]| in U ` implies f . |[a,b]| = 1 ) :: thesis: ( |[a,b]| in U \ {|[x,0 ]|} implies f . |[a,b]| = (|.(|[x,0 ]| - |[a,b]|).| ^2 ) / ((2 * r) * b) )

proof

assume A2: |[a,b]| in U ` ; :: thesis: f . |[a,b]| = 1
then A3: b >= 0 by Lm1, Th22;
not |[a,b]| in U by A2, XBOOLE_0:def 5;
then ( not |[a,b]| in Ball |[x,r]|,r & ( a <> x or b <> 0 ) ) by A1, SETWISEO:6;
hence f . |[a,b]| = 1 by A3, Def5; :: thesis: verum

end;

assume |[a,b]| in U \ {|[x,0 ]|} ; :: thesis: f . |[a,b]| = (|.(|[x,0 ]| - |[a,b]|).| ^2 ) / ((2 * r) * b)
then ( |[a,b]| in U & not |[a,b]| in {|[x,0 ]|} ) by XBOOLE_0:def 5;
then ( b >= 0 & |[a,b]| in Ball |[x,r]|,r ) by A1, Lm1, Th22, XBOOLE_0:def 3;
hence f . |[a,b]| = (|.(|[x,0 ]| - |[a,b]|).| ^2 ) / ((2 * r) * b) by Def5; :: thesis: verum