let x be Element of F_Rat; :: thesis: for x1 being Rational st x <> 0. F_Rat & x1 = x holds
x " = x1 "
let x1 be Rational; :: thesis: ( x <> 0. F_Rat & x1 = x implies x " = x1 " )
assume A1: ( x <> 0. F_Rat & x1 = x ) ; :: thesis: x " = x1 "
reconsider w = x1 " as Element of F_Rat by RAT_1:def 2;
w * x = 1. F_Rat by A1, XCMPLX_0:def 7;
hence x " = x1 " by A1, VECTSP_1:def 10; :: thesis: verum