deffunc H1( Point of (TOP-REAL 2)) -> Element of REAL = (|.(|[x,0 ]| - $1).| ^2 ) / ((2 * r) * ($1 `2 ));
deffunc H2( Point of (TOP-REAL 2)) -> Element of NAT = 1;
deffunc H3( Point of (TOP-REAL 2)) -> Element of NAT = 0 ;
defpred S1[ set ] means not $1 in Ball |[x,r]|,r;
defpred S2[ set ] means $1 = |[x,0 ]|;
A1: for a being Point of (TOP-REAL 2) st a in the carrier of Niemytzki-plane holds
( ( S2[a] implies H3(a) in the carrier of I[01] ) & ( not S2[a] & S1[a] implies H2(a) in the carrier of I[01] ) & ( not S2[a] & not S1[a] implies H1(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 ( ( S2[a] implies H3(a) in the carrier of I[01] ) & ( not S2[a] & S1[a] implies H2(a) in the carrier of I[01] ) & ( not S2[a] & not S1[a] implies H1(a) in the carrier of I[01] ) ) )
assume a in the carrier of Niemytzki-plane ; :: thesis: ( ( S2[a] implies H3(a) in the carrier of I[01] ) & ( not S2[a] & S1[a] implies H2(a) in the carrier of I[01] ) & ( not S2[a] & not S1[a] implies H1(a) in the carrier of I[01] ) )
thus ( S2[a] implies H3(a) in the carrier of I[01] ) by BORSUK_1:83, XXREAL_1:1; :: thesis: ( ( not S2[a] & S1[a] implies H2(a) in the carrier of I[01] ) & ( not S2[a] & not S1[a] implies H1(a) in the carrier of I[01] ) )
thus ( not S2[a] & S1[a] implies H2(a) in the carrier of I[01] ) by BORSUK_1:83, XXREAL_1:1; :: thesis: ( not S2[a] & not S1[a] implies H1(a) in the carrier of I[01] )
assume not S2[a] ; :: thesis: ( S1[a] or H1(a) in the carrier of I[01] )
A2: a = |[(a `1 ),(a `2 )]| by EUCLID:57;
assume not S1[a] ; :: thesis: H1(a) in the carrier of I[01]
then |.(a - |[x,r]|).| < r by TOPREAL9:7;
then |.|[((a `1 ) - x),((a `2 ) - r)]|.| < r by A2, EUCLID:66;
then A3: |.|[((a `1 ) - x),((a `2 ) - r)]|.| ^2 < r ^2 by SQUARE_1:78;
A4: |[((a `1 ) - x),((a `2 ) - r)]| `2 = (a `2 ) - r by EUCLID:56;
|[((a `1 ) - x),((a `2 ) - r)]| `1 = (a `1 ) - x by EUCLID:56;
then (((a `1 ) - x) ^2 ) + (((a `2 ) - r) ^2 ) < r ^2 by A4, A3, JGRAPH_1:46;
then ((((a `1 ) - x) ^2 ) + (((a `2 ) ^2 ) - ((2 * (a `2 )) * r))) + (r ^2 ) < 0 + (r ^2 ) ;
then ((((a `1 ) - x) ^2 ) + ((a `2 ) ^2 )) - ((2 * (a `2 )) * r) < 0 by XREAL_1:8;
then A5: (((a `1 ) - x) ^2 ) + (((a `2 ) - 0 ) ^2 ) < (2 * r) * (a `2 ) by XREAL_1:50;
A6: |[((a `1 ) - x),(a `2 )]| `2 = a `2 by EUCLID:56;
|[((a `1 ) - x),(a `2 )]| `1 = (a `1 ) - x by EUCLID:56;
then A7: |.|[((a `1 ) - x),((a `2 ) - 0 )]|.| ^2 < (2 * r) * (a `2 ) by A6, A5, JGRAPH_1:46;
then |.(a - |[x,0 ]|).| ^2 < (2 * r) * (a `2 ) by A2, EUCLID:66;
then |.(|[x,0 ]| - a).| ^2 < (2 * r) * (a `2 ) by TOPRNS_1:28;
then H1(a) <= 1 by XREAL_1:185;
hence H1(a) in the carrier of I[01] by A7, BORSUK_1:83, XXREAL_1:1; :: thesis: verum
end;
the carrier of Niemytzki-plane = y>=0-plane by Def3;
then A8: the carrier of Niemytzki-plane c= the carrier of (TOP-REAL 2) ;
consider f being Function of Niemytzki-plane ,I[01] such that
A9: for a being Point of (TOP-REAL 2) st a in the carrier of Niemytzki-plane holds
( ( S2[a] implies f . a = H3(a) ) & ( not S2[a] & S1[a] implies f . a = H2(a) ) & ( not S2[a] & not S1[a] implies f . a = H1(a) ) ) from TOPGEN_5:sch 2(A8, A1);
 take f ; :: thesis: ( f . |[x,0 ]| = 0 & ( for a being real number
for b being real non negative number holds
( ( ( a <> x or b <> 0 ) & not |[a,b]| in Ball |[x,r]|,r implies f . |[a,b]| = 1 ) & ( |[a,b]| in Ball |[x,r]|,r implies f . |[a,b]| = (|.(|[x,0 ]| - |[a,b]|).| ^2 ) / ((2 * r) * b) ) ) ) )
A10: the carrier of Niemytzki-plane = y>=0-plane by Def3;
then |[x,0 ]| in the carrier of Niemytzki-plane by Th22;
hence f . |[x,0 ]| = 0 by A9; :: thesis: for a being real number
for b being real non negative number holds
( ( ( a <> x or b <> 0 ) & not |[a,b]| in Ball |[x,r]|,r implies f . |[a,b]| = 1 ) & ( |[a,b]| in Ball |[x,r]|,r implies f . |[a,b]| = (|.(|[x,0 ]| - |[a,b]|).| ^2 ) / ((2 * r) * b) ) )
let a be real number ; :: thesis: for b being real non negative number holds
( ( ( a <> x or b <> 0 ) & not |[a,b]| in Ball |[x,r]|,r implies f . |[a,b]| = 1 ) & ( |[a,b]| in Ball |[x,r]|,r implies f . |[a,b]| = (|.(|[x,0 ]| - |[a,b]|).| ^2 ) / ((2 * r) * b) ) )
let b be real non negative number ; :: thesis: ( ( ( a <> x or b <> 0 ) & not |[a,b]| in Ball |[x,r]|,r implies f . |[a,b]| = 1 ) & ( |[a,b]| in Ball |[x,r]|,r implies f . |[a,b]| = (|.(|[x,0 ]| - |[a,b]|).| ^2 ) / ((2 * r) * b) ) )
A11: |[a,b]| in the carrier of Niemytzki-plane by A10, Th22;
hereby :: thesis: ( |[a,b]| in Ball |[x,r]|,r implies f . |[a,b]| = (|.(|[x,0 ]| - |[a,b]|).| ^2 ) / ((2 * r) * b) )
assume ( a <> x or b <> 0 ) ; :: thesis: ( not |[a,b]| in Ball |[x,r]|,r implies f . |[a,b]| = 1 )
then not S2[|[a,b]|] by SPPOL_2:1;
hence ( not |[a,b]| in Ball |[x,r]|,r implies f . |[a,b]| = 1 ) by A9, A11; :: thesis: verum
end;
assume A12: |[a,b]| in Ball |[x,r]|,r ; :: thesis: f . |[a,b]| = (|.(|[x,0 ]| - |[a,b]|).| ^2 ) / ((2 * r) * b)
A13: |[x,0 ]| in y=0-line by Th19;
A14: |[a,b]| `2 = b by EUCLID:56;
Ball |[x,r]|,r misses y=0-line by Th25;
then not S2[|[a,b]|] by A13, A12, XBOOLE_0:3;
hence f . |[a,b]| = (|.(|[x,0 ]| - |[a,b]|).| ^2 ) / ((2 * r) * b) by A14, A9, A11, A12; :: thesis: verum