:: deftheorem Def2 defines * ARYTM_0:def 2 :
for x, y, b₃ being Element of REAL holds
( ( x in REAL+ & y in REAL+ implies ( b₃ = * (x,y) iff ex x9, y9 being Element of REAL+ st
( x = x9 & y = y9 & b₃ = x9 *' y9 ) ) ) & ( x in REAL+ & y in [:{0},REAL+:] & x <> 0 implies ( b₃ = * (x,y) iff ex x9, y9 being Element of REAL+ st
( x = x9 & y = [0,y9] & b₃ = [0,(x9 *' y9)] ) ) ) & ( y in REAL+ & x in [:{0},REAL+:] & y <> 0 implies ( b₃ = * (x,y) iff ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = y9 & b₃ = [0,(y9 *' x9)] ) ) ) & ( x in [:{0},REAL+:] & y in [:{0},REAL+:] implies ( b₃ = * (x,y) iff ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = [0,y9] & b₃ = y9 *' x9 ) ) ) & ( ( 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+:] ) implies ( b₃ = * (x,y) iff b₃ = 0 ) ) );