let f, g be Function of Niemytzki-plane ,I[01] ; :: thesis: ( ( for a being real number
for b being real non negative number 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 number
for b being real non negative number 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 number
for b being real non negative number 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 number
for b being real non negative number 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 ) ) ; :: thesis: f = g
A7: 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 A7;
then reconsider q = p as Point of (TOP-REAL 2) ;
A8: p = |[(q `1 ),(q `2 )]| by EUCLID:57;
then reconsider q2 = q `2 as real non negative number by A7, Th22;

per cases ( not |[(q `1 ),q2]| in Ball |[x,y]|,r or |[(q `1 ),q2]| in Ball |[x,y]|,r ) ;

suppose A9: not |[(q `1 ),q2]| in Ball |[x,y]|,r ; :: thesis: f . b₁ = g . b₁

then f . p = 1 by A5, A8;
hence f . p = g . p by A9, A6, A8; :: thesis: verum

end;

suppose A10: |[(q `1 ),q2]| in Ball |[x,y]|,r ; :: thesis: f . b₁ = g . b₁

then f . p = |.(|[x,y]| - q).| / r by A5, A8;
hence f . p = g . p by A10, A6, A8; :: thesis: verum

end;

end;

end;

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