let K be Field; :: thesis: for p being Element of (Polynom-Ring K) st p <> 0_. K holds
p is non zero Element of the carrier of (Polynom-Ring K)
let p be Element of (Polynom-Ring K); :: thesis: ( p <> 0_. K implies p is non zero Element of the carrier of (Polynom-Ring K) )
assume A0: p <> 0_. K ; :: thesis: p is non zero Element of the carrier of (Polynom-Ring K)
assume A1: p is not non zero Element of the carrier of (Polynom-Ring K) ; :: thesis: contradiction
reconsider p = p as Element of the carrier of (Polynom-Ring K) ;
p is zero by A1;
hence contradiction by A0; :: thesis: verum