let L be non empty almost_left_invertible well-unital distributive associative commutative doubleLoopStr ; :: thesis: for p being Polynomial of L st len p <> 0 holds
(NormPolynomial p) . ((len p) -' 1) = 1. L
let p be Polynomial of L; :: thesis: ( len p <> 0 implies (NormPolynomial p) . ((len p) -' 1) = 1. L )
assume len p <> 0 ; :: thesis: (NormPolynomial p) . ((len p) -' 1) = 1. L
then len p >= 0 + 1 by NAT_1:13;
then len p = ((len p) -' 1) + 1 by XREAL_1:235;
then A1: p . ((len p) -' 1) <> 0. L by ALGSEQ_1:10;
thus (NormPolynomial p) . ((len p) -' 1) = (p . ((len p) -' 1)) / (p . ((len p) -' 1)) by Def11
.= (p . ((len p) -' 1)) * ((p . ((len p) -' 1)) ")
.= 1. L by A1, VECTSP_1:def 10 ; :: thesis: verum