let U be Subset of Niemytzki-plane; :: thesis: for x being Real
for r being positive Real 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 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 Real; :: thesis: for r being positive Real 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 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 positive Real; :: 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 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 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 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 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; :: 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: not |[a,b]| in U by XBOOLE_0:def 5;
then A4: not |[a,b]| in Ball (|[x,r]|,r) by A1, ZFMISC_1:136;
A5: ( a <> x or b <> 0 ) by A3, A1, ZFMISC_1:136;
b >= 0 by A2, Lm1, Th18;
hence f . |[a,b]| = 1 by A4, A5, Def5; :: thesis: verum

end;

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