thus ( x <> 0 implies ex y being Element of REAL st * (x,y) = 1 ) :: thesis: ( not x <> 0 implies ex b₁ being Element of REAL st b₁ = 0 )

proof

A46: x in REAL+ \/ [:{0},REAL+:] by XBOOLE_0:def 5;
assume A47: x <> 0 ; :: thesis: ex y being Element of REAL st * (x,y) = 1

per cases ( x in REAL+ or x in [:{0},REAL+:] ) by A46, XBOOLE_0:def 3;

suppose x in REAL+ ; :: thesis: ex y being Element of REAL st * (x,y) = 1

then reconsider x9 = x as Element of REAL+ ;
reconsider jj = 1 as Element of REAL by NUMBERS:19;
consider y9 being Element of REAL+ such that
A48: x9 *' y9 = jj by A47, ARYTM_2:14;
reconsider y = y9 as Element of REAL by Th1;
take y ; :: thesis: * (x,y) = 1
thus * (x,y) = 1 by A48, Def2; :: thesis: verum

end;

suppose A49: x in [:{0},REAL+:] ; :: thesis: ex y being Element of REAL st * (x,y) = 1

not x in {[0,0]} by XBOOLE_0:def 5;
then A50: x <> [0,0] by TARSKI:def 1;
consider x1, x2 being object such that
x1 in {0} and
A51: x2 in REAL+ and
A52: x = [x1,x2] by A49, ZFMISC_1:84;
reconsider x2 = x2 as Element of REAL+ by A51;
x1 in {0} by A49, A52, ZFMISC_1:87;
then x2 <> 0 by A52, A50, TARSKI:def 1;
then consider y2 being Element of REAL+ such that
A53: x2 *' y2 = 1 by ARYTM_2:14;

A54: now :: thesis: not [0,y2] in {[0,0]}

assume [0,y2] in {[0,0]} ; :: thesis: contradiction
then [0,y2] = [0,0] by TARSKI:def 1;
then y2 = 0 by XTUPLE_0:1;
hence contradiction by A53, ARYTM_2:4; :: thesis: verum

end;

A55: [0,y2] in [:{0},REAL+:] by Lm1;
then [0,y2] in REAL+ \/ [:{0},REAL+:] by XBOOLE_0:def 3;
then reconsider y = [0,y2] as Element of REAL by A54, XBOOLE_0:def 5;
take y ; :: thesis: * (x,y) = 1
consider x9, y9 being Element of REAL+ such that
A56: x = [0,x9] and
A57: y = [0,y9] and
A58: * (x,y) = y9 *' x9 by A49, A55, Def2;
y9 = y2 by A57, XTUPLE_0:1;
hence * (x,y) = 1 by A52, A53, A56, A58, XTUPLE_0:1; :: thesis: verum

end;

end;

end;

thus ( not x <> 0 implies ex b₁ being Element of REAL st b₁ = 0 ) ; :: thesis: verum