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 XTUPLE_0:1; :: 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 XTUPLE_0:1; :: 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, XTUPLE_0:1;
hence IT1 = IT2 by A37, A39, XTUPLE_0:1; :: 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