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

end;

assume x in REAL+ ; :: thesis:
then reconsider x9 = x as Element of REAL+ ;
assume y in [:{0},REAL+:] ; :: thesis:
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 ; :: thesis:
then reconsider IT = [0,(x9 *' y9)] as Element of REAL by A25, Th2, ARYTM_1:2;
take IT = IT; :: thesis:
take x9 = x9; :: thesis:
take y9 = y9; :: thesis:
thus ( x = x9 & y = [0,y9] & IT = [0,(x9 *' y9)] ) by A22, A24, TARSKI:def 1; :: thesis:

end;

assume y in REAL+ ; :: thesis:
then reconsider y9 = y as Element of REAL+ ;
assume x in [:{0},REAL+:] ; :: thesis:
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 ; :: thesis:
then reconsider IT = [0,(y9 *' x9)] as Element of REAL by A29, Th2, ARYTM_1:2;
take IT = IT; :: thesis:
take x9 = x9; :: thesis:
take y9 = y9; :: thesis:
thus ( x = [0,x9] & y = y9 & IT = [0,(y9 *' x9)] ) by A26, A28, TARSKI:def 1; :: thesis:

end;

assume x in [:{0},REAL+:] ; :: thesis:
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+:] ; :: thesis:
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; :: thesis:
take x9 = x9; :: thesis:
take y9 = y9; :: thesis:
thus ( x = [0,x9] & y = [0,y9] & IT = y9 *' x9 ) by A30, A32, A33, A35, TARSKI:def 1; :: thesis:

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 ) by Lm3; :: thesis: