let n be Nat; :: thesis: for L being non empty ZeroStr
for z being Element of L st z <> 0. L holds
for p being Polynomial of L st p = (0_. L) +* (n,z) holds
deg p = n
let L be non empty ZeroStr ; :: thesis: for z being Element of L st z <> 0. L holds
for p being Polynomial of L st p = (0_. L) +* (n,z) holds
deg p = n
let z be Element of L; :: thesis: ( z <> 0. L implies for p being Polynomial of L st p = (0_. L) +* (n,z) holds
deg p = n )
assume A1: z <> 0. L ; :: thesis: for p being Polynomial of L st p = (0_. L) +* (n,z) holds
deg p = n
let p be Polynomial of L; :: thesis: ( p = (0_. L) +* (n,z) implies deg p = n )
assume p = (0_. L) +* (n,z) ; :: thesis: deg p = n
hence deg p = (n + 1) - 1 by A1, Th18
.= n ;
:: thesis: verum