let U be Subset of Niemytzki-plane ; :: thesis: for x, y being Element of REAL
for r being real positive number st y > 0 & U = (Ball |[x,y]|,r) /\ y>=0-plane holds
ex f being continuous Function of Niemytzki-plane ,I[01] st
( f . |[x,y]| = 0 & ( for a, b being real number holds
( ( |[a,b]| in U ` implies f . |[a,b]| = 1 ) & ( |[a,b]| in U implies f . |[a,b]| = |.(|[x,y]| - |[a,b]|).| / r ) ) ) )
let x, y be Element of REAL ; :: thesis: for r being real positive number st y > 0 & U = (Ball |[x,y]|,r) /\ y>=0-plane holds
ex f being continuous Function of Niemytzki-plane ,I[01] st
( f . |[x,y]| = 0 & ( for a, b being real number holds
( ( |[a,b]| in U ` implies f . |[a,b]| = 1 ) & ( |[a,b]| in U implies f . |[a,b]| = |.(|[x,y]| - |[a,b]|).| / r ) ) ) )
let r be real positive number ; :: thesis: ( y > 0 & U = (Ball |[x,y]|,r) /\ y>=0-plane implies ex f being continuous Function of Niemytzki-plane ,I[01] st
( f . |[x,y]| = 0 & ( for a, b being real number holds
( ( |[a,b]| in U ` implies f . |[a,b]| = 1 ) & ( |[a,b]| in U implies f . |[a,b]| = |.(|[x,y]| - |[a,b]|).| / r ) ) ) ) )
assume that
A1: y > 0 and
A2: U = (Ball |[x,y]|,r) /\ y>=0-plane ; :: thesis: ex f being continuous Function of Niemytzki-plane ,I[01] st
( f . |[x,y]| = 0 & ( for a, b being real number holds
( ( |[a,b]| in U ` implies f . |[a,b]| = 1 ) & ( |[a,b]| in U implies f . |[a,b]| = |.(|[x,y]| - |[a,b]|).| / r ) ) ) )
reconsider y9 = y as real positive number by A1;
take f = + x,y9,r; :: thesis: ( f . |[x,y]| = 0 & ( for a, b being real number holds
( ( |[a,b]| in U ` implies f . |[a,b]| = 1 ) & ( |[a,b]| in U implies f . |[a,b]| = |.(|[x,y]| - |[a,b]|).| / r ) ) ) )
|[x,y9]| `2 = y by EUCLID:56;
hence f . |[x,y]| = 0 by Th81; :: thesis: for a, b being real number holds
( ( |[a,b]| in U ` implies f . |[a,b]| = 1 ) & ( |[a,b]| in U implies f . |[a,b]| = |.(|[x,y]| - |[a,b]|).| / r ) )
let a, b be real number ; :: thesis: ( ( |[a,b]| in U ` implies f . |[a,b]| = 1 ) & ( |[a,b]| in U implies f . |[a,b]| = |.(|[x,y]| - |[a,b]|).| / r ) )
thus ( |[a,b]| in U ` implies f . |[a,b]| = 1 ) :: thesis: ( |[a,b]| in U implies f . |[a,b]| = |.(|[x,y]| - |[a,b]|).| / r )

proof

assume A3: |[a,b]| in U ` ; :: thesis: f . |[a,b]| = 1
then not |[a,b]| in U by XBOOLE_0:def 5;
then A4: not |[a,b]| in Ball |[x,y]|,r by A2, A3, Lm1, XBOOLE_0:def 4;
b >= 0 by A3, Lm1, Th22;
hence f . |[a,b]| = 1 by A4, Def6; :: thesis: verum

end;

assume A5: |[a,b]| in U ; :: thesis: f . |[a,b]| = |.(|[x,y]| - |[a,b]|).| / r
then A6: |[a,b]| in Ball |[x,y]|,r by A2, XBOOLE_0:def 4;
b >= 0 by A5, Lm1, Th22;
hence f . |[a,b]| = |.(|[x,y]| - |[a,b]|).| / r by A6, Def6; :: thesis: verum