theorem Th14: :: POLYNOM3:14

for n, i being Element of NAT st i in Seg (n + 1) holds
(Decomp (n,2)) . i = <*(i -' 1),((n + 1) -' i)*>