hereby :: thesis: ( ( x in REAL+ & y in [:{0 },REAL+ :] & x <> 0 implies ex b₁ being Element of REAL ex x', y' being Element of REAL+ st
( x = x' & y = [0 ,y'] & b₁ = [0 ,(x' *' y')] ) ) & ( y in REAL+ & x in [:{0 },REAL+ :] & y <> 0 implies ex b₁ being Element of REAL ex x', y' being Element of REAL+ st
( x = [0 ,x'] & y = y' & b₁ = [0 ,(y' *' x')] ) ) & ( x in [:{0 },REAL+ :] & y in [:{0 },REAL+ :] implies ex b₁ being Element of REAL ex x', y' being Element of REAL+ st
( x = [0 ,x'] & y = [0 ,y'] & b₁ = 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 b₁ being Element of REAL st b₁ = 0 ) )

assume ( x in REAL+ & y in REAL+ ) ; :: thesis: ex IT being Element of REAL ex x', y' being Element of REAL+ st
( x = x' & y = y' & IT = x' *' y' )
then reconsider x' = x, y' = y as Element of REAL+ ;
x' *' y' in REAL+ ;
then reconsider IT = x' *' y' as Element of REAL by Th1;
take IT = IT; :: thesis: ex x', y' being Element of REAL+ st
( x = x' & y = y' & IT = x' *' y' )
take x' = x'; :: thesis: ex y' being Element of REAL+ st
( x = x' & y = y' & IT = x' *' y' )
take y' = y'; :: thesis: ( x = x' & y = y' & IT = x' *' y' )
thus ( x = x' & y = y' & IT = x' *' y' ) ; :: thesis: verum

end;

hereby :: thesis: ( ( y in REAL+ & x in [:{0 },REAL+ :] & y <> 0 implies ex b₁ being Element of REAL ex x', y' being Element of REAL+ st
( x = [0 ,x'] & y = y' & b₁ = [0 ,(y' *' x')] ) ) & ( x in [:{0 },REAL+ :] & y in [:{0 },REAL+ :] implies ex b₁ being Element of REAL ex x', y' being Element of REAL+ st
( x = [0 ,x'] & y = [0 ,y'] & b₁ = 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 b₁ being Element of REAL st b₁ = 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
A22: z in {0 } and
A23: y' in REAL+ and
A24: y = [z,y'] by ZFMISC_1:103;
reconsider y' = y' as Element of REAL+ by A23;
y = [0 ,y'] by A22, A24, TARSKI:def 1;
then A25: y' <> 0 by Th3;
assume 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')] )
then reconsider IT = [0 ,(x' *' y')] as Element of REAL by A25, 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 A22, A24, TARSKI:def 1; :: thesis: verum

end;

hereby :: thesis: ( ( x in [:{0 },REAL+ :] & y in [:{0 },REAL+ :] implies ex b₁ being Element of REAL ex x', y' being Element of REAL+ st
( x = [0 ,x'] & y = [0 ,y'] & b₁ = 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 b₁ being Element of REAL st b₁ = 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
A26: z in {0 } and
A27: x' in REAL+ and
A28: x = [z,x'] by ZFMISC_1:103;
reconsider x' = x' as Element of REAL+ by A27;
x = [0 ,x'] by A26, A28, TARSKI:def 1;
then A29: x' <> 0 by Th3;
assume 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')] )
then reconsider IT = [0 ,(y' *' x')] as Element of REAL by A29, 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 A26, A28, 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 b₁ being Element of REAL st b₁ = 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
A30: z1 in {0 } and
A31: x' in REAL+ and
A32: x = [z1,x'] by ZFMISC_1:103;
reconsider x' = x' as Element of REAL+ by A31;
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
A33: z2 in {0 } and
A34: y' in REAL+ and
A35: y = [z2,y'] by ZFMISC_1:103;
reconsider y' = y' as Element of REAL+ by A34;
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 A30, A32, A33, A35, 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 b₁ being Element of REAL st b₁ = 0 ) ; :: thesis: verum