let U be Subset of Niemytzki-plane; 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; 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; ( 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]|}
; 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); ( 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; 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; ( ( |[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 )
( |[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 `
;
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;
verum
end;
assume A6:
|[a,b]| in U \ {|[x,0]|}
; 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; verum