let IT1, IT2 be Element of REAL ; ( ( 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 )
; ( ( 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; ( ( 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; ( ( 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 ( ( 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+:]
;
( 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 )
;
( 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 )
;
IT1 = IT2
x9 = x99
by A36, A38, XTUPLE_0:1;
hence
IT1 = IT2
by A37, A39, XTUPLE_0:1;
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 )
; verum