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 )
assume A1: ( x * y = 0. F_Real & x <> 0. F_Real ) ; :: thesis: y = 0. F_Real
reconsider x' = x, y' = y as Real ;
0. F_Real = 0 by STRUCT_0:def 6;
hence y = 0. F_Real by A1, XCMPLX_1:6; :: thesis: verum

end;