let U be Subset of Niemytzki-plane; :: thesis: for x, y being Real
for r being positive Real 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 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 Real; :: thesis: for r being positive Real 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 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 positive Real; :: 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 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 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 positive Real by A1;
take f = + (x,y9,r); :: thesis: ( f . |[x,y]| = 0 & ( for a, b being Real 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:52;
hence f . |[x,y]| = 0 by Th77; :: thesis: for a, b being Real 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; :: 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, Th18;
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, Th18;
hence f . |[a,b]| = |.(|[x,y]| - |[a,b]|).| / r by A6, Def6; :: thesis: verum