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