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

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

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

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

then reconsider x' = x as Element of REAL+ ;
consider y' being Element of REAL+ such that
A55: x' *' y' = 1 by A52, ARYTM_2:15;
y' in REAL+ ;
then reconsider y = y' as Element of REAL by Th1;
take y ; :: thesis: * x,y = 1
consider x'', y'' being Element of REAL+ such that
A56: x = x'' and
A57: y = y'' and
A58: * x,y = x'' *' y'' by A54, Def3;
thus * x,y = 1 by A55, A56, A57, A58; :: thesis: verum

end;

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

then consider x1, x2 being set such that
x1 in {0 } and
A60: x2 in REAL+ and
A61: x = [x1,x2] by ZFMISC_1:103;
reconsider x2 = x2 as Element of REAL+ by A60;
not x in {[0 ,0 ]} by NUMBERS:def 1, XBOOLE_0:def 5;
then A62: x <> [0 ,0 ] by TARSKI:def 1;
x1 in {0 } by A59, A61, ZFMISC_1:106;
then x2 <> 0 by A61, A62, TARSKI:def 1;
then consider y2 being Element of REAL+ such that
A63: x2 *' y2 = 1 by ARYTM_2:15;
A64: [0 ,y2] in [:{0 },REAL+ :] by Lm1, ZFMISC_1:106;
then A65: [0 ,y2] in REAL+ \/ [:{0 },REAL+ :] by XBOOLE_0:def 3;

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 A63, ARYTM_2:4; :: thesis: verum

end;

then reconsider y = [0 ,y2] as Element of REAL by A65, NUMBERS:def 1, XBOOLE_0:def 5;
consider x', y' being Element of REAL+ such that
A66: x = [0 ,x'] and
A67: y = [0 ,y'] and
A68: * x,y = y' *' x' by A59, A64, Def3;
take y ; :: thesis: * x,y = 1
( y' = y2 & x' = x2 ) by A61, A66, A67, ZFMISC_1:33;
hence * x,y = 1 by A63, A68; :: thesis: verum

end;

end;

end;

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