hereby ( ( x in REAL+ & y in [:{0},REAL+:] & x <> 0 implies ex b1 being Element of REAL ex x9, y9 being Element of REAL+ st
( x = x9 & y = [0,y9] & b1 = [0,(x9 *' y9)] ) ) & ( y in REAL+ & x in [:{0},REAL+:] & y <> 0 implies ex b1 being Element of REAL ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = y9 & b1 = [0,(y9 *' x9)] ) ) & ( x in [:{0},REAL+:] & y in [:{0},REAL+:] implies ex b1 being Element of REAL ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = [0,y9] & b1 = 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 ex b1 being Element of REAL st b1 = 0 ) )
end;
hereby ( ( y in REAL+ & x in [:{0},REAL+:] & y <> 0 implies ex b1 being Element of REAL ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = y9 & b1 = [0,(y9 *' x9)] ) ) & ( x in [:{0},REAL+:] & y in [:{0},REAL+:] implies ex b1 being Element of REAL ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = [0,y9] & b1 = 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 ex b1 being Element of REAL st b1 = 0 ) )
assume
x in REAL+
;
( y in [:{0},REAL+:] & x <> 0 implies ex IT being Element of REAL ex x9, y9 being Element of REAL+ st
( x = x9 & y = [0,y9] & IT = [0,(x9 *' y9)] ) )then reconsider x9 =
x as
Element of
REAL+ ;
assume
y in [:{0},REAL+:]
;
( x <> 0 implies ex IT being Element of REAL ex x9, y9 being Element of REAL+ st
( x = x9 & y = [0,y9] & IT = [0,(x9 *' y9)] ) )then consider z,
y9 being
object such that A22:
z in {0}
and A23:
y9 in REAL+
and A24:
y = [z,y9]
by ZFMISC_1:84;
reconsider y9 =
y9 as
Element of
REAL+ by A23;
y = [0,y9]
by A22, A24, TARSKI:def 1;
then A25:
y9 <> 0
by Th3;
assume
x <> 0
;
ex IT being Element of REAL ex x9, y9 being Element of REAL+ st
( x = x9 & y = [0,y9] & IT = [0,(x9 *' y9)] )then reconsider IT =
[0,(x9 *' y9)] as
Element of
REAL by A25, Th2, ARYTM_1:2;
take IT =
IT;
ex x9, y9 being Element of REAL+ st
( x = x9 & y = [0,y9] & IT = [0,(x9 *' y9)] )take x9 =
x9;
ex y9 being Element of REAL+ st
( x = x9 & y = [0,y9] & IT = [0,(x9 *' y9)] )take y9 =
y9;
( x = x9 & y = [0,y9] & IT = [0,(x9 *' y9)] )thus
(
x = x9 &
y = [0,y9] &
IT = [0,(x9 *' y9)] )
by A22, A24, TARSKI:def 1;
verum
end;
hereby ( ( x in [:{0},REAL+:] & y in [:{0},REAL+:] implies ex b1 being Element of REAL ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = [0,y9] & b1 = 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 ex b1 being Element of REAL st b1 = 0 ) )
assume
y in REAL+
;
( x in [:{0},REAL+:] & y <> 0 implies ex IT being Element of REAL ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = y9 & IT = [0,(y9 *' x9)] ) )then reconsider y9 =
y as
Element of
REAL+ ;
assume
x in [:{0},REAL+:]
;
( y <> 0 implies ex IT being Element of REAL ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = y9 & IT = [0,(y9 *' x9)] ) )then consider z,
x9 being
object such that A26:
z in {0}
and A27:
x9 in REAL+
and A28:
x = [z,x9]
by ZFMISC_1:84;
reconsider x9 =
x9 as
Element of
REAL+ by A27;
x = [0,x9]
by A26, A28, TARSKI:def 1;
then A29:
x9 <> 0
by Th3;
assume
y <> 0
;
ex IT being Element of REAL ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = y9 & IT = [0,(y9 *' x9)] )then reconsider IT =
[0,(y9 *' x9)] as
Element of
REAL by A29, Th2, ARYTM_1:2;
take IT =
IT;
ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = y9 & IT = [0,(y9 *' x9)] )take x9 =
x9;
ex y9 being Element of REAL+ st
( x = [0,x9] & y = y9 & IT = [0,(y9 *' x9)] )take y9 =
y9;
( x = [0,x9] & y = y9 & IT = [0,(y9 *' x9)] )thus
(
x = [0,x9] &
y = y9 &
IT = [0,(y9 *' x9)] )
by A26, A28, TARSKI:def 1;
verum
end;
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+:] ) implies ex b1 being Element of REAL st b1 = 0 )
assume
x in [:{0},REAL+:]
;
( y in [:{0},REAL+:] implies ex IT being Element of REAL ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = [0,y9] & IT = y9 *' x9 ) )then consider z1,
x9 being
object such that A30:
z1 in {0}
and A31:
x9 in REAL+
and A32:
x = [z1,x9]
by ZFMISC_1:84;
reconsider x9 =
x9 as
Element of
REAL+ by A31;
assume
y in [:{0},REAL+:]
;
ex IT being Element of REAL ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = [0,y9] & IT = y9 *' x9 )then consider z2,
y9 being
object such that A33:
z2 in {0}
and A34:
y9 in REAL+
and A35:
y = [z2,y9]
by ZFMISC_1:84;
reconsider y9 =
y9 as
Element of
REAL+ by A34;
reconsider IT =
y9 *' x9 as
Element of
REAL by Th1;
take IT =
IT;
ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = [0,y9] & IT = y9 *' x9 )take x9 =
x9;
ex y9 being Element of REAL+ st
( x = [0,x9] & y = [0,y9] & IT = y9 *' x9 )take y9 =
y9;
( x = [0,x9] & y = [0,y9] & IT = y9 *' x9 )thus
(
x = [0,x9] &
y = [0,y9] &
IT = y9 *' x9 )
by A30, A32, A33, A35, TARSKI:def 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+:] ) implies ex b1 being Element of REAL st b1 = 0 )
by Lm3; verum