let L be non empty ZeroStr ; :: thesis: for p being Polynomial of L st len p = 1 holds
p = <%(p . 0)%>
let p be Polynomial of L; :: thesis: ( len p = 1 implies p = <%(p . 0)%> )
assume A1: len p = 1 ; :: thesis: p = <%(p . 0)%>
( p . ((len p) -' 1) <> 0. L & (len p) -' 1 = 0 ) by A1, UPROOTS:18, XREAL_1:232;
then A2: len <%(p . 0)%> = 1 by POLYNOM5:33;
for k being Nat st k < len p holds
p . k = <%(p . 0)%> . k

proof

let k be Nat; :: thesis: ( k < len p implies p . k = <%(p . 0)%> . k )
assume k < len p ; :: thesis: p . k = <%(p . 0)%> . k
then k = 0 by A1, NAT_1:14;
hence p . k = <%(p . 0)%> . k by POLYNOM5:32; :: thesis: verum

end;

hence p = <%(p . 0)%> by A1, A2, ALGSEQ_1:12; :: thesis: verum