theorem :: ALGGEO_1:8

for R being domRing
for n being non empty Ordinal
for a being non zero Element of R
for b being Element of R
for i being Element of n holds ((a | (n,R)) *' (1_1 (i,R))) + (b | (n,R)) is Polynomial of n,R ;