defpred S₁[ set ] means not $1 in Ball |[x,y]|,r;
deffunc H₁( Point of (TOP-REAL 2)) -> Element of REAL = |.(|[x,y]| - $1).| / r;
deffunc H₂( Point of (TOP-REAL 2)) -> Element of NAT = 1;
the carrier of Niemytzki-plane = y>=0-plane by Def3;
then A1: the carrier of Niemytzki-plane c= the carrier of (TOP-REAL 2) ;
A2: for a being Point of (TOP-REAL 2) st a in the carrier of Niemytzki-plane holds
( ( S₁[a] implies H₂(a) in the carrier of I[01] ) & ( not S₁[a] implies H₁(a) in the carrier of I[01] ) )

proof

let a be Point of (TOP-REAL 2); :: thesis: ( a in the carrier of Niemytzki-plane implies ( ( S₁[a] implies H₂(a) in the carrier of I[01] ) & ( not S₁[a] implies H₁(a) in the carrier of I[01] ) ) )
assume a in the carrier of Niemytzki-plane ; :: thesis: ( ( S₁[a] implies H₂(a) in the carrier of I[01] ) & ( not S₁[a] implies H₁(a) in the carrier of I[01] ) )
thus ( S₁[a] implies H₂(a) in the carrier of I[01] ) by BORSUK_1:83, XXREAL_1:1; :: thesis: ( not S₁[a] implies H₁(a) in the carrier of I[01] )
assume not S₁[a] ; :: thesis: H₁(a) in the carrier of I[01]
then |.(a - |[x,y]|).| < r by TOPREAL9:7;
then ( |.(|[x,y]| - a).| < r & |.(|[x,y]| - a).| >= 0 ) by TOPRNS_1:28;
then ( 0 / r <= H₁(a) & H₁(a) < r / r & r / r = 1 ) by XCMPLX_1:60, XREAL_1:76;
hence H₁(a) in the carrier of I[01] by BORSUK_1:83, XXREAL_1:1; :: thesis: verum

end;

consider f being Function of Niemytzki-plane ,I[01] such that
A3: for a being Point of (TOP-REAL 2) st a in the carrier of Niemytzki-plane holds
( ( S₁[a] implies f . a = H₂(a) ) & ( not S₁[a] implies f . a = H₁(a) ) ) from TOPGEN_5:sch 1(A1, A2);
take f ; :: thesis: for a being real number
for b being real non negative number holds
( ( not |[a,b]| in Ball |[x,y]|,r implies f . |[a,b]| = 1 ) & ( |[a,b]| in Ball |[x,y]|,r implies f . |[a,b]| = |.(|[x,y]| - |[a,b]|).| / r ) )
let a be real number ; :: thesis: for b being real non negative number holds
( ( not |[a,b]| in Ball |[x,y]|,r implies f . |[a,b]| = 1 ) & ( |[a,b]| in Ball |[x,y]|,r implies f . |[a,b]| = |.(|[x,y]| - |[a,b]|).| / r ) )
let b be real non negative number ; :: thesis: ( ( not |[a,b]| in Ball |[x,y]|,r implies f . |[a,b]| = 1 ) & ( |[a,b]| in Ball |[x,y]|,r implies f . |[a,b]| = |.(|[x,y]| - |[a,b]|).| / r ) )
|[a,b]| in the carrier of Niemytzki-plane by Lm1, Th22;
hence ( ( not |[a,b]| in Ball |[x,y]|,r implies f . |[a,b]| = 1 ) & ( |[a,b]| in Ball |[x,y]|,r implies f . |[a,b]| = |.(|[x,y]| - |[a,b]|).| / r ) ) by A3; :: thesis: verum