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

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