let y, z be Element of REAL ; :: thesis: ( ( x <> 0 & * x,y = 1 & * x,z = 1 implies y = z ) & ( not x <> 0 & y = 0 & z = 0 implies y = z ) )
thus ( x <> 0 & * x,y = 1 & * x,z = 1 implies y = z ) :: thesis: ( not x <> 0 & y = 0 & z = 0 implies y = z )

proof

assume that
A69: x <> 0 and
A70: * x,y = 1 and
A71: * x,z = 1 ; :: thesis: y = z
A72: for x, y being Element of REAL st * x,y = 1 holds
x <> 0

proof

let x, y be Element of REAL ; :: thesis: ( * x,y = 1 implies x <> 0 )
assume that
A73: * x,y = 1 and
A74: x = 0 ; :: thesis: contradiction
A75: not x in [:{0 },REAL+ :] by A74, Th5, ARYTM_2:21, XBOOLE_0:3;
A76: y in REAL+ \/ [:{0 },REAL+ :] by NUMBERS:def 1, XBOOLE_0:def 5;

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

suppose y in REAL+ ; :: thesis: contradiction

then ex x', y' being Element of REAL+ st
( x = x' & y = y' & 1 = x' *' y' ) by A73, A74, Def3, ARYTM_2:21;
hence contradiction by A74, ARYTM_2:4; :: thesis: verum

end;

suppose y in [:{0 },REAL+ :] ; :: thesis: contradiction

then not y in REAL+ by Th5, XBOOLE_0:3;
hence contradiction by A73, A74, A75, Def3; :: thesis: verum

end;

end;

end;

then A77: y <> 0 by A70;
A78: z <> 0 by A71, A72;

per cases ( ( x in REAL+ & y in REAL+ & z in REAL+ ) or ( x in [:{0 },REAL+ :] & y in [:{0 },REAL+ :] & z in [:{0 },REAL+ :] ) or ( x in REAL+ & y in [:{0 },REAL+ :] ) or ( x in [:{0 },REAL+ :] & y in REAL+ ) or ( x in [:{0 },REAL+ :] & z in REAL+ ) or ( x in REAL+ & z in [:{0 },REAL+ :] ) or ( ( 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+ :] ) ) or ( ( not x in REAL+ or not z in REAL+ ) & ( not x in REAL+ or not z in [:{0 },REAL+ :] or not x <> 0 ) & ( not z in REAL+ or not x in [:{0 },REAL+ :] or not z <> 0 ) & ( not x in [:{0 },REAL+ :] or not z in [:{0 },REAL+ :] ) ) ) ;

suppose ( x in REAL+ & y in REAL+ & z in REAL+ ) ; :: thesis: y = z

then ( ex x', y' being Element of REAL+ st
( x = x' & y = y' & 1 = x' *' y' ) & ex x', y' being Element of REAL+ st
( x = x' & z = y' & 1 = x' *' y' ) ) by A70, A71, Def3;
hence y = z by A69, Th8; :: thesis: verum

end;

suppose that A79: x in [:{0 },REAL+ :] and
A80: y in [:{0 },REAL+ :] and
A81: z in [:{0 },REAL+ :] ; :: thesis: y = z

consider x', y' being Element of REAL+ such that
A82: x = [0 ,x'] and
A83: y = [0 ,y'] and
A84: 1 = y' *' x' by A70, A79, A80, Def3;
consider x'', z' being Element of REAL+ such that
A85: x = [0 ,x''] and
A86: z = [0 ,z'] and
A87: 1 = z' *' x'' by A71, A79, A81, Def3;
x' = x'' by A82, A85, ZFMISC_1:33;
hence y = z by A82, A83, A84, A86, A87, Th3, Th8; :: thesis: verum

end;

suppose ( x in REAL+ & y in [:{0 },REAL+ :] ) ; :: thesis: y = z

then ex x', y' being Element of REAL+ st
( x = x' & y = [0 ,y'] & 1 = [0 ,(x' *' y')] ) by A69, A70, Def3;
hence y = z by Th7; :: thesis: verum

end;

suppose ( x in [:{0 },REAL+ :] & y in REAL+ ) ; :: thesis: y = z

then ex x', y' being Element of REAL+ st
( x = [0 ,x'] & y = y' & 1 = [0 ,(y' *' x')] ) by A70, A77, Def3;
hence y = z by Th7; :: thesis: verum

end;

suppose ( x in [:{0 },REAL+ :] & z in REAL+ ) ; :: thesis: y = z

then ex x', z' being Element of REAL+ st
( x = [0 ,x'] & z = z' & 1 = [0 ,(z' *' x')] ) by A71, A78, Def3;
hence y = z by Th7; :: thesis: verum

end;

suppose ( x in REAL+ & z in [:{0 },REAL+ :] ) ; :: thesis: y = z

then ex x', z' being Element of REAL+ st
( x = x' & z = [0 ,z'] & 1 = [0 ,(x' *' z')] ) by A69, A71, Def3;
hence y = z by Th7; :: thesis: verum

end;

suppose ( ( 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+ :] ) ) ; :: thesis: y = z

hence y = z by A70, Def3; :: thesis: verum

end;

suppose ( ( not x in REAL+ or not z in REAL+ ) & ( not x in REAL+ or not z in [:{0 },REAL+ :] or not x <> 0 ) & ( not z in REAL+ or not x in [:{0 },REAL+ :] or not z <> 0 ) & ( not x in [:{0 },REAL+ :] or not z in [:{0 },REAL+ :] ) ) ; :: thesis: y = z

hence y = z by A71, Def3; :: thesis: verum

end;

end;

end;

thus ( not x <> 0 & y = 0 & z = 0 implies y = z ) ; :: thesis: verum