let F be non empty right_complementable almost_left_invertible add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr ; :: thesis: for x, y being Element of F holds
( x * y = 0. F iff ( x = 0. F or y = 0. F ) )
let x, y be Element of F; :: thesis: ( x * y = 0. F iff ( x = 0. F or y = 0. F ) )
( not x * y = 0. F or x = 0. F or y = 0. F )

proof

assume A1: x * y = 0. F ; :: thesis: ( x = 0. F or y = 0. F )
assume A2: x <> 0. F ; :: thesis: y = 0. F
(x ") * (0. F) = ((x ") * x) * y by A1, GROUP_1:def 3
.= (1. F) * y by A2, Def10
.= y ;
hence y = 0. F ; :: thesis: verum

end;

hence ( x * y = 0. F iff ( x = 0. F or y = 0. F ) ) ; :: thesis: verum