let L be non empty ZeroStr ; :: thesis: for p being Polynomial of L st p <> 0_. L holds
(len p) -' 1 = (len p) - 1
let p be Polynomial of L; :: thesis: ( p <> 0_. L implies (len p) -' 1 = (len p) - 1 )
assume p <> 0_. L ; :: thesis: (len p) -' 1 = (len p) - 1
then 0 <> len p by POLYNOM4:5;
then 0 + 1 <= len p by NAT_1:13;
hence (len p) -' 1 = (len p) - 1 by XREAL_1:233; :: thesis: verum