let IT1, IT2 be Element of REAL ; :: thesis: ( ( x in REAL+ & y in REAL+ & ex x9, y9 being Element of REAL+ st
( x = x9 & y = y9 & IT1 = x9 *' y9 ) & ex x9, y9 being Element of REAL+ st
( x = x9 & y = y9 & IT2 = x9 *' y9 ) implies IT1 = IT2 ) & ( x in REAL+ & y in [:{0 },REAL+ :] & x <> 0 & ex x9, y9 being Element of REAL+ st
( x = x9 & y = [0 ,y9] & IT1 = [0 ,(x9 *' y9)] ) & ex x9, y9 being Element of REAL+ st
( x = x9 & y = [0 ,y9] & IT2 = [0 ,(x9 *' y9)] ) implies IT1 = IT2 ) & ( y in REAL+ & x in [:{0 },REAL+ :] & y <> 0 & ex x9, y9 being Element of REAL+ st
( x = [0 ,x9] & y = y9 & IT1 = [0 ,(y9 *' x9)] ) & ex x9, y9 being Element of REAL+ st
( x = [0 ,x9] & y = y9 & IT2 = [0 ,(y9 *' x9)] ) implies IT1 = IT2 ) & ( x in [:{0 },REAL+ :] & y in [:{0 },REAL+ :] & ex x9, y9 being Element of REAL+ st
( x = [0 ,x9] & y = [0 ,y9] & IT1 = y9 *' x9 ) & ex x9, y9 being Element of REAL+ st
( x = [0 ,x9] & y = [0 ,y9] & IT2 = y9 *' x9 ) 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 x9, y9 being Element of REAL+ st
( x = x9 & y = y9 & IT1 = x9 *' y9 ) & ex x9, y9 being Element of REAL+ st
( x = x9 & y = y9 & IT2 = x9 *' y9 ) implies IT1 = IT2 ) ; :: thesis: ( ( x in REAL+ & y in [:{0 },REAL+ :] & x <> 0 & ex x9, y9 being Element of REAL+ st
( x = x9 & y = [0 ,y9] & IT1 = [0 ,(x9 *' y9)] ) & ex x9, y9 being Element of REAL+ st
( x = x9 & y = [0 ,y9] & IT2 = [0 ,(x9 *' y9)] ) implies IT1 = IT2 ) & ( y in REAL+ & x in [:{0 },REAL+ :] & y <> 0 & ex x9, y9 being Element of REAL+ st
( x = [0 ,x9] & y = y9 & IT1 = [0 ,(y9 *' x9)] ) & ex x9, y9 being Element of REAL+ st
( x = [0 ,x9] & y = y9 & IT2 = [0 ,(y9 *' x9)] ) implies IT1 = IT2 ) & ( x in [:{0 },REAL+ :] & y in [:{0 },REAL+ :] & ex x9, y9 being Element of REAL+ st
( x = [0 ,x9] & y = [0 ,y9] & IT1 = y9 *' x9 ) & ex x9, y9 being Element of REAL+ st
( x = [0 ,x9] & y = [0 ,y9] & IT2 = y9 *' x9 ) 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 x9, y9 being Element of REAL+ st
( x = x9 & y = [0 ,y9] & IT1 = [0 ,(x9 *' y9)] ) & ex x99, y99 being Element of REAL+ st
( x = x99 & y = [0 ,y99] & IT2 = [0 ,(x99 *' y99)] ) implies IT1 = IT2 ) by ZFMISC_1:33; :: thesis: ( ( y in REAL+ & x in [:{0 },REAL+ :] & y <> 0 & ex x9, y9 being Element of REAL+ st
( x = [0 ,x9] & y = y9 & IT1 = [0 ,(y9 *' x9)] ) & ex x9, y9 being Element of REAL+ st
( x = [0 ,x9] & y = y9 & IT2 = [0 ,(y9 *' x9)] ) implies IT1 = IT2 ) & ( x in [:{0 },REAL+ :] & y in [:{0 },REAL+ :] & ex x9, y9 being Element of REAL+ st
( x = [0 ,x9] & y = [0 ,y9] & IT1 = y9 *' x9 ) & ex x9, y9 being Element of REAL+ st
( x = [0 ,x9] & y = [0 ,y9] & IT2 = y9 *' x9 ) 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 x9, y9 being Element of REAL+ st
( x = [0 ,x9] & y = y9 & IT1 = [0 ,(y9 *' x9)] ) & ex x99, y99 being Element of REAL+ st
( x = [0 ,x99] & y = y99 & IT2 = [0 ,(y99 *' x99)] ) implies IT1 = IT2 ) by ZFMISC_1:33; :: thesis: ( ( x in [:{0 },REAL+ :] & y in [:{0 },REAL+ :] & ex x9, y9 being Element of REAL+ st
( x = [0 ,x9] & y = [0 ,y9] & IT1 = y9 *' x9 ) & ex x9, y9 being Element of REAL+ st
( x = [0 ,x9] & y = [0 ,y9] & IT2 = y9 *' x9 ) 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 x9, y9 being Element of REAL+ st
( x = [0 ,x9] & y = [0 ,y9] & IT1 = y9 *' x9 ) & ex x99, y99 being Element of REAL+ st
( x = [0 ,x99] & y = [0 ,y99] & IT2 = y99 *' x99 ) implies IT1 = IT2 )
given x9, y9 being Element of REAL+ such that A36: x = [0 ,x9] and
A37: ( y = [0 ,y9] & IT1 = y9 *' x9 ) ; :: thesis: ( ex x99, y99 being Element of REAL+ st
( x = [0 ,x99] & y = [0 ,y99] & IT2 = y99 *' x99 ) implies IT1 = IT2 )
given x99, y99 being Element of REAL+ such that A38: x = [0 ,x99] and
A39: ( y = [0 ,y99] & IT2 = y99 *' x99 ) ; :: thesis: IT1 = IT2
x9 = x99 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