set D = F_Real ;

hereby :: according to VECTSP_2:def 5 :: thesis: verum

let x, y be Element of F_Real; :: thesis: ( x * y = 0. F_Real & x <> 0. F_Real implies y = 0. F_Real )
A1: 0. F_Real = 0 by STRUCT_0:def 6;
assume ( x * y = 0. F_Real & x <> 0. F_Real ) ; :: thesis: y = 0. F_Real
hence y = 0. F_Real by A1, XCMPLX_1:6; :: thesis: verum

end;