let f, g be Function of Niemytzki-plane,I[01]; :: thesis: ( ( for a being Real
for b being non negative Real 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 ) ) ) & ( for a being Real
for b being non negative Real holds
( ( not |[a,b]| in Ball (|[x,y]|,r) implies g . |[a,b]| = 1 ) & ( |[a,b]| in Ball (|[x,y]|,r) implies g . |[a,b]| = |.(|[x,y]| - |[a,b]|).| / r ) ) ) implies f = g )
assume that
A5: for a being Real
for b being non negative Real 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 ) ) and
A6: for a being Real
for b being non negative Real holds
( ( not |[a,b]| in Ball (|[x,y]|,r) implies g . |[a,b]| = 1 ) & ( |[a,b]| in Ball (|[x,y]|,r) implies g . |[a,b]| = |.(|[x,y]| - |[a,b]|).| / r ) ) ; :: thesis: f = g
A7: the carrier of Niemytzki-plane = y>=0-plane by Def3;

now :: thesis: for p being Point of Niemytzki-plane holds f . p = g . p

let p be Point of Niemytzki-plane; :: thesis: f . b₁ = g . b₁
p in y>=0-plane by A7;
then reconsider q = p as Point of (TOP-REAL 2) ;
A8: p = |[(q `1),(q `2)]| by EUCLID:53;
then reconsider q2 = q `2 as non negative Real by A7, Th18;

per cases ( not |[(q `1),q2]| in Ball (|[x,y]|,r) or |[(q `1),q2]| in Ball (|[x,y]|,r) ) ;

suppose A9: not |[(q `1),q2]| in Ball (|[x,y]|,r) ; :: thesis: f . b₁ = g . b₁

then f . p = 1 by A5, A8;
hence f . p = g . p by A9, A6, A8; :: thesis: verum

end;

suppose A10: |[(q `1),q2]| in Ball (|[x,y]|,r) ; :: thesis: f . b₁ = g . b₁

then f . p = |.(|[x,y]| - q).| / r by A5, A8;
hence f . p = g . p by A10, A6, A8; :: thesis: verum

end;

end;

end;

hence f = g ; :: thesis: verum