let f, g be Function of Niemytzki-plane,I[01]; ( f . |[x,0]| = 0 & ( for a being Real
for b being non negative Real 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) ) ) ) & g . |[x,0]| = 0 & ( for a being Real
for b being non negative Real holds
( ( ( a <> x or b <> 0 ) & not |[a,b]| in Ball (|[x,r]|,r) implies g . |[a,b]| = 1 ) & ( |[a,b]| in Ball (|[x,r]|,r) implies g . |[a,b]| = (|.(|[x,0]| - |[a,b]|).| ^2) / ((2 * r) * b) ) ) ) implies f = g )
assume that
A15:
f . |[x,0]| = 0
and
A16:
for a being Real
for b being non negative Real 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) ) )
and
A17:
g . |[x,0]| = 0
and
A18:
for a being Real
for b being non negative Real holds
( ( ( a <> x or b <> 0 ) & not |[a,b]| in Ball (|[x,r]|,r) implies g . |[a,b]| = 1 ) & ( |[a,b]| in Ball (|[x,r]|,r) implies g . |[a,b]| = (|.(|[x,0]| - |[a,b]|).| ^2) / ((2 * r) * b) ) )
; f = g
A19:
the carrier of Niemytzki-plane = y>=0-plane
by Def3;
hence
f = g
; verum