let x be Element of INT ; :: thesis: for y being Element of F_Real st x <> 0 & x = y holds
x " = y "
let y be Element of F_Real; :: thesis: ( x <> 0 & x = y implies x " = y " )
assume B1: ( x <> 0 & x = y ) ; :: thesis: x " = y "
reconsider xi = x " as Element of F_Real by XREAL_0:def 1;
X2: xi * y = 1. F_Real by B1, XCMPLX_0:def 7;
y <> 0. F_Real by B1;
hence x " = y " by X2, VECTSP_1:def 10; :: thesis: verum