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:20, XBOOLE_0:3;
A66: y in REAL+ \/ [:{0},REAL+:] by 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, Def2, ARYTM_2:20;
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, Def2; :: 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, Def2;
hence y = z by A59, Th7; :: 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, Def2;
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, Def2;
x9 = x99 by A72, A74, XTUPLE_0:1;
hence y = z by A72, A73, A75, Th3, Th7; :: 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, Def2;
hence y = z by Lm2; :: 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, Def2;
hence y = z by Lm2; :: 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, Def2;
hence y = z by Lm2; :: 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, Def2;
hence y = z by Lm2; :: 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, Def2; :: 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, Def2; :: thesis: verum

end;

end;

end;

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