let n be Ordinal; :: thesis: for T being connected TermOrder of n
for L being non empty ZeroStr
for p being Polynomial of n,L holds Support p in Fin the carrier of RelStr(# (Bags n),T #)
let T be connected TermOrder of n; :: thesis: for L being non empty ZeroStr
for p being Polynomial of n,L holds Support p in Fin the carrier of RelStr(# (Bags n),T #)
let L be non empty ZeroStr ; :: thesis: for p being Polynomial of n,L holds Support p in Fin the carrier of RelStr(# (Bags n),T #)
let p be Polynomial of n,L; :: thesis: Support p in Fin the carrier of RelStr(# (Bags n),T #)
set sp = Support p;
Support p is finite by POLYNOM1:def 5;
hence Support p in Fin the carrier of RelStr(# (Bags n),T #) by FINSUB_1:def 5; :: thesis: verum