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
A59: x <> 0 and
A60: * x,y = 1 and
A61: * x,z = 1 ; :: thesis: y = z
A62: 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
A63: * x,y = 1 and
A64: x = 0 ; :: thesis: contradiction
A65: not x in [:{0 },REAL+ :] by A64, Th5, ARYTM_2:21, XBOOLE_0:3;
A66: y in REAL+ \/ [:{0 },REAL+ :] by NUMBERS:def 1, XBOOLE_0:def 5;

per cases ( y in REAL+ or y in [:{0 },REAL+ :] ) by A66, 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 A63, A64, Def3, ARYTM_2:21;
hence contradiction by A64, 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 A63, A64, A65, Def3; :: thesis: verum

end;

end;

end;

then A67: y <> 0 by A60;
A68: z <> 0 by A61, A62;

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 A60, A61, Def3;
hence y = z by A59, Th8; :: thesis: verum

end;

suppose that A69: x in [:{0 },REAL+ :] and
A70: y in [:{0 },REAL+ :] and
A71: z in [:{0 },REAL+ :] ; :: thesis: y = z

consider x', y' being Element of REAL+ such that
A72: x = [0 ,x'] and
A73: ( y = [0 ,y'] & 1 = y' *' x' ) by A60, A69, A70, Def3;
consider x'', z' being Element of REAL+ such that
A74: x = [0 ,x''] and
A75: ( z = [0 ,z'] & 1 = z' *' x'' ) by A61, A69, A71, Def3;
x' = x'' by A72, A74, ZFMISC_1:33;
hence y = z by A72, A73, A75, 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 A59, A60, 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 A60, A67, 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 A61, A68, 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 A59, A61, 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 A60, 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 A61, Def3; :: thesis: verum

end;

end;

end;

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