let f, g be Function of Niemytzki-plane,I[01]; :: thesis: ( 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) ) ) ; :: thesis: f = g
A19: 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 A19;
then reconsider q = p as Point of (TOP-REAL 2) ;
A20: p = |[(q `1),(q `2)]| by EUCLID:53;
then reconsider q2 = q `2 as non negative Real by A19, Th18;

per cases ( ( q `1 = x & q2 = 0 ) or ( ( q `1 <> x or q2 <> 0 ) & not |[(q `1),q2]| in Ball (|[x,r]|,r) ) or p in Ball (|[x,r]|,r) ) by EUCLID:53;

suppose ( q `1 = x & q2 = 0 ) ; :: thesis: f . b₁ = g . b₁

hence f . p = g . p by A15, A17, A20; :: thesis: verum

end;

suppose A21: ( ( q `1 <> x or q2 <> 0 ) & not |[(q `1),q2]| in Ball (|[x,r]|,r) ) ; :: thesis: f . b₁ = g . b₁

then f . p = 1 by A16, A20;
hence f . p = g . p by A18, A20, A21; :: thesis: verum

end;

suppose A22: p in Ball (|[x,r]|,r) ; :: thesis: f . b₁ = g . b₁

then f . p = (|.(|[x,0]| - q).| ^2) / ((2 * r) * q2) by A16, A20;
hence f . p = g . p by A18, A20, A22; :: thesis: verum

end;

end;

end;

hence f = g ; :: thesis: verum