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 A1: ( y > 0 & 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 ) ) ) )
then reconsider y' = y as real positive number ;
take f = + x,y',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,y']| `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 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,y]|,r by A1, A2, Lm1, XBOOLE_0:def 4;
hence f . |[a,b]| = 1 by A3, Def6; :: thesis: verum

end;

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