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 x9, y9 being Element of REAL+ st
( x = x9 & y = y9 & 1 = x9 *' y9 ) 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 x9, y9 being Element of REAL+ st
( x = x9 & y = y9 & 1 = x9 *' y9 ) & ex x9, y9 being Element of REAL+ st
( x = x9 & z = y9 & 1 = x9 *' y9 ) ) 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 x9, y9 being Element of REAL+ such that
A72: x = [0 ,x9] and
A73: ( y = [0 ,y9] & 1 = y9 *' x9 ) by A60, A69, A70, Def3;
consider x99, z9 being Element of REAL+ such that
A74: x = [0 ,x99] and
A75: ( z = [0 ,z9] & 1 = z9 *' x99 ) by A61, A69, A71, Def3;
x9 = x99 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 x9, y9 being Element of REAL+ st
( x = x9 & y = [0 ,y9] & 1 = [0 ,(x9 *' y9)] ) 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 x9, y9 being Element of REAL+ st
( x = [0 ,x9] & y = y9 & 1 = [0 ,(y9 *' x9)] ) 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 x9, z9 being Element of REAL+ st
( x = [0 ,x9] & z = z9 & 1 = [0 ,(z9 *' x9)] ) 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 x9, z9 being Element of REAL+ st
( x = x9 & z = [0 ,z9] & 1 = [0 ,(x9 *' z9)] ) 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