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 NUMBERS:def 1, 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+ ;
consider y9 being Element of REAL+ such that
A48: x9 *' y9 = 1 by A47, ARYTM_2:15;
y9 in REAL+ ;
then reconsider y = y9 as Element of REAL by Th1;
take y ; :: thesis: * x,y = 1
thus * x,y = 1 by A48, Def3; :: 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 NUMBERS:def 1, XBOOLE_0:def 5;
then A50: x <> [0 ,0 ] by TARSKI:def 1;
consider x1, x2 being set such that
x1 in {0 } and
A51: x2 in REAL+ and
A52: x = [x1,x2] by A49, ZFMISC_1:103;
reconsider x2 = x2 as Element of REAL+ by A51;
x1 in {0 } by A49, A52, ZFMISC_1:106;
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:15;

A54: now

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

end;

A55: [0 ,y2] in [:{0 },REAL+ :] by Lm1, ZFMISC_1:106;
then [0 ,y2] in REAL+ \/ [:{0 },REAL+ :] by XBOOLE_0:def 3;
then reconsider y = [0 ,y2] as Element of REAL by A54, NUMBERS:def 1, 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, Def3;
y9 = y2 by A57, ZFMISC_1:33;
hence * x,y = 1 by A52, A53, A56, A58, ZFMISC_1:33; :: thesis: verum

end;

end;

end;

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