let IT1, IT2 be Element of REAL ; :: thesis: ( ( x in REAL+ & y in REAL+ & ex x', y' being Element of REAL+ st
( x = x' & y = y' & IT1 = x' *' y' ) & ex x', y' being Element of REAL+ st
( x = x' & y = y' & IT2 = x' *' y' ) implies IT1 = IT2 ) & ( x in REAL+ & y in [:{0 },REAL+ :] & x <> 0 & ex x', y' being Element of REAL+ st
( x = x' & y = [0 ,y'] & IT1 = [0 ,(x' *' y')] ) & ex x', y' being Element of REAL+ st
( x = x' & y = [0 ,y'] & IT2 = [0 ,(x' *' y')] ) implies IT1 = IT2 ) & ( y in REAL+ & x in [:{0 },REAL+ :] & y <> 0 & ex x', y' being Element of REAL+ st
( x = [0 ,x'] & y = y' & IT1 = [0 ,(y' *' x')] ) & ex x', y' being Element of REAL+ st
( x = [0 ,x'] & y = y' & IT2 = [0 ,(y' *' x')] ) implies IT1 = IT2 ) & ( x in [:{0 },REAL+ :] & y in [:{0 },REAL+ :] & ex x', y' being Element of REAL+ st
( x = [0 ,x'] & y = [0 ,y'] & IT1 = y' *' x' ) & ex x', y' being Element of REAL+ st
( x = [0 ,x'] & y = [0 ,y'] & IT2 = y' *' x' ) implies IT1 = IT2 ) & ( ( not x in REAL+ or not y in REAL+ ) & ( not x in REAL+ or not y in [:{0 },REAL+ :] or not x <> 0 ) & ( not y in REAL+ or not x in [:{0 },REAL+ :] or not y <> 0 ) & ( not x in [:{0 },REAL+ :] or not y in [:{0 },REAL+ :] ) & IT1 = 0 & IT2 = 0 implies IT1 = IT2 ) )
thus ( x in REAL+ & y in REAL+ & ex x', y' being Element of REAL+ st
( x = x' & y = y' & IT1 = x' *' y' ) & ex x', y' being Element of REAL+ st
( x = x' & y = y' & IT2 = x' *' y' ) implies IT1 = IT2 ) ; :: thesis: ( ( x in REAL+ & y in [:{0 },REAL+ :] & x <> 0 & ex x', y' being Element of REAL+ st
( x = x' & y = [0 ,y'] & IT1 = [0 ,(x' *' y')] ) & ex x', y' being Element of REAL+ st
( x = x' & y = [0 ,y'] & IT2 = [0 ,(x' *' y')] ) implies IT1 = IT2 ) & ( y in REAL+ & x in [:{0 },REAL+ :] & y <> 0 & ex x', y' being Element of REAL+ st
( x = [0 ,x'] & y = y' & IT1 = [0 ,(y' *' x')] ) & ex x', y' being Element of REAL+ st
( x = [0 ,x'] & y = y' & IT2 = [0 ,(y' *' x')] ) implies IT1 = IT2 ) & ( x in [:{0 },REAL+ :] & y in [:{0 },REAL+ :] & ex x', y' being Element of REAL+ st
( x = [0 ,x'] & y = [0 ,y'] & IT1 = y' *' x' ) & ex x', y' being Element of REAL+ st
( x = [0 ,x'] & y = [0 ,y'] & IT2 = y' *' x' ) implies IT1 = IT2 ) & ( ( not x in REAL+ or not y in REAL+ ) & ( not x in REAL+ or not y in [:{0 },REAL+ :] or not x <> 0 ) & ( not y in REAL+ or not x in [:{0 },REAL+ :] or not y <> 0 ) & ( not x in [:{0 },REAL+ :] or not y in [:{0 },REAL+ :] ) & IT1 = 0 & IT2 = 0 implies IT1 = IT2 ) )
thus ( x in REAL+ & y in [:{0 },REAL+ :] & x <> 0 & ex x', y' being Element of REAL+ st
( x = x' & y = [0 ,y'] & IT1 = [0 ,(x' *' y')] ) & ex x'', y'' being Element of REAL+ st
( x = x'' & y = [0 ,y''] & IT2 = [0 ,(x'' *' y'')] ) implies IT1 = IT2 ) by ZFMISC_1:33; :: thesis: ( ( y in REAL+ & x in [:{0 },REAL+ :] & y <> 0 & ex x', y' being Element of REAL+ st
( x = [0 ,x'] & y = y' & IT1 = [0 ,(y' *' x')] ) & ex x', y' being Element of REAL+ st
( x = [0 ,x'] & y = y' & IT2 = [0 ,(y' *' x')] ) implies IT1 = IT2 ) & ( x in [:{0 },REAL+ :] & y in [:{0 },REAL+ :] & ex x', y' being Element of REAL+ st
( x = [0 ,x'] & y = [0 ,y'] & IT1 = y' *' x' ) & ex x', y' being Element of REAL+ st
( x = [0 ,x'] & y = [0 ,y'] & IT2 = y' *' x' ) implies IT1 = IT2 ) & ( ( not x in REAL+ or not y in REAL+ ) & ( not x in REAL+ or not y in [:{0 },REAL+ :] or not x <> 0 ) & ( not y in REAL+ or not x in [:{0 },REAL+ :] or not y <> 0 ) & ( not x in [:{0 },REAL+ :] or not y in [:{0 },REAL+ :] ) & IT1 = 0 & IT2 = 0 implies IT1 = IT2 ) )
thus ( y in REAL+ & x in [:{0 },REAL+ :] & y <> 0 & ex x', y' being Element of REAL+ st
( x = [0 ,x'] & y = y' & IT1 = [0 ,(y' *' x')] ) & ex x'', y'' being Element of REAL+ st
( x = [0 ,x''] & y = y'' & IT2 = [0 ,(y'' *' x'')] ) implies IT1 = IT2 ) by ZFMISC_1:33; :: thesis: ( ( x in [:{0 },REAL+ :] & y in [:{0 },REAL+ :] & ex x', y' being Element of REAL+ st
( x = [0 ,x'] & y = [0 ,y'] & IT1 = y' *' x' ) & ex x', y' being Element of REAL+ st
( x = [0 ,x'] & y = [0 ,y'] & IT2 = y' *' x' ) implies IT1 = IT2 ) & ( ( not x in REAL+ or not y in REAL+ ) & ( not x in REAL+ or not y in [:{0 },REAL+ :] or not x <> 0 ) & ( not y in REAL+ or not x in [:{0 },REAL+ :] or not y <> 0 ) & ( not x in [:{0 },REAL+ :] or not y in [:{0 },REAL+ :] ) & IT1 = 0 & IT2 = 0 implies IT1 = IT2 ) )

hereby :: thesis: ( ( not x in REAL+ or not y in REAL+ ) & ( not x in REAL+ or not y in [:{0 },REAL+ :] or not x <> 0 ) & ( not y in REAL+ or not x in [:{0 },REAL+ :] or not y <> 0 ) & ( not x in [:{0 },REAL+ :] or not y in [:{0 },REAL+ :] ) & IT1 = 0 & IT2 = 0 implies IT1 = IT2 )

assume that
x in [:{0 },REAL+ :] and
y in [:{0 },REAL+ :] ; :: thesis: ( ex x', y' being Element of REAL+ st
( x = [0 ,x'] & y = [0 ,y'] & IT1 = y' *' x' ) & ex x'', y'' being Element of REAL+ st
( x = [0 ,x''] & y = [0 ,y''] & IT2 = y'' *' x'' ) implies IT1 = IT2 )
given x', y' being Element of REAL+ such that A36: x = [0 ,x'] and
A37: ( y = [0 ,y'] & IT1 = y' *' x' ) ; :: thesis: ( ex x'', y'' being Element of REAL+ st
( x = [0 ,x''] & y = [0 ,y''] & IT2 = y'' *' x'' ) implies IT1 = IT2 )
given x'', y'' being Element of REAL+ such that A38: x = [0 ,x''] and
A39: ( y = [0 ,y''] & IT2 = y'' *' x'' ) ; :: thesis: IT1 = IT2
x' = x'' by A36, A38, ZFMISC_1:33;
hence IT1 = IT2 by A37, A39, ZFMISC_1:33; :: thesis: verum

end;

thus ( ( not x in REAL+ or not y in REAL+ ) & ( not x in REAL+ or not y in [:{0 },REAL+ :] or not x <> 0 ) & ( not y in REAL+ or not x in [:{0 },REAL+ :] or not y <> 0 ) & ( not x in [:{0 },REAL+ :] or not y in [:{0 },REAL+ :] ) & IT1 = 0 & IT2 = 0 implies IT1 = IT2 ) ; :: thesis: verum