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
A8: ( 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) ) ) ) ) and
A9: ( 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) ) ) ) ) ; :: thesis: f = g
A10: 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 A10;
then reconsider q = p as Point of (TOP-REAL 2) ;
A11: p = |[(q `1 ),(q `2 )]| by EUCLID:57;
then reconsider q2 = q `2 as real non negative number by A10, 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 A8, A9, A11; :: thesis: verum

end;

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

then ( f . p = 1 & g . p = 1 ) by A8, A9, A11;
hence f . p = g . p ; :: thesis: verum

end;

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

then ( f . p = (|.(|[x,0 ]| - q).| ^2 ) / ((2 * r) * q2) & g . p = (|.(|[x,0 ]| - q).| ^2 ) / ((2 * r) * q2) ) by A8, A9, A11;
hence f . p = g . p ; :: thesis: verum

end;

end;

end;

hence f = g by FUNCT_2:113; :: thesis: verum