let f, g be Function of Niemytzki-plane,I[01]; ( ( 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 ) )
; f = g
A7:
the carrier of Niemytzki-plane = y>=0-plane
by Def3;
hence
f = g
; verum