let p be Prime; :: thesis: for a, b being Element of (GF p) holds
( ( a = 0 or b = 0 ) iff a * b = 0 )
let a, b be Element of (GF p); :: thesis: ( ( a = 0 or b = 0 ) iff a * b = 0 )
( ( a = 0. (GF p) or b = 0. (GF p) ) iff a * b = 0. (GF p) ) by VECTSP_1:12;
hence ( ( a = 0 or b = 0 ) iff a * b = 0 ) ; :: thesis: verum