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

proof

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

end;

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