set S = Subst (t,x,p);
set P = p `^ (t . x);
reconsider SP = Support (p `^ (t . x)) as finite set by POLYNOM1:def 5;
set ordP = canFS SP;
A1: rng (canFS SP) = Support (p `^ (t . x)) by FUNCT_2:def 3;
then reconsider ordP = canFS SP as FinSequence of Bags O by FINSEQ_1:def 4;
deffunc H<sub>1</sub>( object ) -> bag of O = Subst (t,x,(ordP /. O));
consider ordS being FinSequence such that
A2: len ordS = len ordP and
A3: for k being Nat st k in dom ordS holds
ordS . k = H<sub>1</sub>(k) from FINSEQ_1:sch 2();
A4: dom ordS = dom ordP by A2, FINSEQ_3:29;
A5: ( dom (Subst (t,x,p)) = Bags O & Bags O = dom (p `^ (t . x)) ) by FUNCT_2:def 1;
Support (Subst (t,x,p)) c= rng ordS

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Support (Subst (t,x,p)) or y in rng ordS )
assume A6: y in Support (Subst (t,x,p)) ; :: thesis: y in rng ordS
reconsider y = y as bag of O by A6;
A7: (Subst (t,x,p)) . y <> 0. R by A6, POLYNOM1:def 3;
then consider s being bag of O such that
A8: y = Subst (t,x,s) by Def3;
A9: s in dom (p `^ (t . x)) by A5, PRE_POLY:def 12;
(p `^ (t . x)) . s <> 0. R by A7, A8, Th33;
then s in Support (p `^ (t . x)) by A9, POLYNOM1:def 3;
then consider i being object such that
A10: ( i in dom ordP & ordP . i = s ) by A1, FUNCT_1:def 3;
reconsider i = i as Nat by A10;
ordP /. i = s by A10, PARTFUN1:def 6;
then ordS . i = Subst (t,x,s) by A3, A10, A4;
hence y in rng ordS by A8, A10, A4, FUNCT_1:def 3; :: thesis: verum

end;

hence Subst (t,x,p) is finite-Support by POLYNOM1:def 5; :: thesis: verum