let f, g be Function of Niemytzki-plane ,I[01] ; :: 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) ) ) ) & g . |[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 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 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) ) ) and
A17: g . |[x,0 ]| = 0 and
A18: 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 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

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:57;
then reconsider q2 = q `2 as real non negative number by A19, Th22;

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:57;

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 by FUNCT_2:113; :: thesis: verum