let x be object ; :: thesis: for O being Ordinal
for R being non trivial right_complementable add-associative right_zeroed right_unital distributive doubleLoopStr
for p being Polynomial of O,R
for t being bag of O
for ordP being one-to-one FinSequence of Bags O st rng ordP = Support (p `^ (t . x)) holds
ex ordS being one-to-one FinSequence of Bags O st
( rng ordS = Support (Subst (t,x,p)) & len ordS = len ordP & ( for j being Nat st 1 <= j & j <= len ordS holds
ordS . j = Subst (t,x,(ordP /. j)) ) )
let O be Ordinal; :: thesis: for R being non trivial right_complementable add-associative right_zeroed right_unital distributive doubleLoopStr
for p being Polynomial of O,R
for t being bag of O
for ordP being one-to-one FinSequence of Bags O st rng ordP = Support (p `^ (t . x)) holds
ex ordS being one-to-one FinSequence of Bags O st
( rng ordS = Support (Subst (t,x,p)) & len ordS = len ordP & ( for j being Nat st 1 <= j & j <= len ordS holds
ordS . j = Subst (t,x,(ordP /. j)) ) )
let R be non trivial right_complementable add-associative right_zeroed right_unital distributive doubleLoopStr ; :: thesis: for p being Polynomial of O,R
for t being bag of O
for ordP being one-to-one FinSequence of Bags O st rng ordP = Support (p `^ (t . x)) holds
ex ordS being one-to-one FinSequence of Bags O st
( rng ordS = Support (Subst (t,x,p)) & len ordS = len ordP & ( for j being Nat st 1 <= j & j <= len ordS holds
ordS . j = Subst (t,x,(ordP /. j)) ) )
let p be Polynomial of O,R; :: thesis: for t being bag of O
for ordP being one-to-one FinSequence of Bags O st rng ordP = Support (p `^ (t . x)) holds
ex ordS being one-to-one FinSequence of Bags O st
( rng ordS = Support (Subst (t,x,p)) & len ordS = len ordP & ( for j being Nat st 1 <= j & j <= len ordS holds
ordS . j = Subst (t,x,(ordP /. j)) ) )
let t be bag of O; :: thesis: for ordP being one-to-one FinSequence of Bags O st rng ordP = Support (p `^ (t . x)) holds
ex ordS being one-to-one FinSequence of Bags O st
( rng ordS = Support (Subst (t,x,p)) & len ordS = len ordP & ( for j being Nat st 1 <= j & j <= len ordS holds
ordS . j = Subst (t,x,(ordP /. j)) ) )
set S = Subst (t,x,p);
set P = p `^ (t . x);
let ordP be one-to-one FinSequence of Bags O; :: thesis: ( rng ordP = Support (p `^ (t . x)) implies ex ordS being one-to-one FinSequence of Bags O st
( rng ordS = Support (Subst (t,x,p)) & len ordS = len ordP & ( for j being Nat st 1 <= j & j <= len ordS holds
ordS . j = Subst (t,x,(ordP /. j)) ) ) )
assume A1: rng ordP = Support (p `^ (t . x)) ; :: thesis: ex ordS being one-to-one FinSequence of Bags O st
( rng ordS = Support (Subst (t,x,p)) & len ordS = len ordP & ( for j being Nat st 1 <= j & j <= len ordS holds
ordS . j = Subst (t,x,(ordP /. j)) ) )
deffunc H₁( object ) -> bag of O = Subst (t,x,(ordP /. $1));
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₁(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;
A6: rng ordS c= Support (Subst (t,x,p))

proof

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

end;

then reconsider ordS = ordS as FinSequence of Bags O by FINSEQ_1:def 4, XBOOLE_1:1;
A11: 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 A12: y in Support (Subst (t,x,p)) ; :: thesis: y in rng ordS
reconsider y = y as bag of O by A12;
A13: (Subst (t,x,p)) . y <> 0. R by A12, POLYNOM1:def 3;
then consider s being bag of O such that
A14: y = Subst (t,x,s) by Def3;
A15: s in dom (p `^ (t . x)) by A5, PRE_POLY:def 12;
(Subst (t,x,p)) . y = (p `^ (t . x)) . s by A14, Th33;
then s in Support (p `^ (t . x)) by A13, A15, POLYNOM1:def 3;
then consider i being object such that
A16: ( i in dom ordP & ordP . i = s ) by A1, FUNCT_1:def 3;
reconsider i = i as Nat by A16;
ordP /. i = s by A16, PARTFUN1:def 6;
then ordS . i = y by A14, A3, A16, A4;
hence y in rng ordS by A16, A4, FUNCT_1:def 3; :: thesis: verum

end;

ordS is one-to-one

proof

let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in dom ordS or not x2 in dom ordS or not ordS . x1 = ordS . x2 or x1 = x2 )
assume A17: ( x1 in dom ordS & x2 in dom ordS & ordS . x1 = ordS . x2 ) ; :: thesis: x1 = x2
( ordS . x1 = H₁(x1) & ordS . x2 = H₁(x2) ) by A3, A17;
then ( ordP . x1 = ordP /. x1 & ordP /. x1 = ordP /. x2 & ordP /. x2 = ordP . x2 ) by A4, PARTFUN1:def 6, Th32, A17;
hence x1 = x2 by A17, A4, FUNCT_1:def 4; :: thesis: verum

end;

then reconsider ordS = ordS as one-to-one FinSequence of Bags O ;
take ordS ; :: thesis: ( rng ordS = Support (Subst (t,x,p)) & len ordS = len ordP & ( for j being Nat st 1 <= j & j <= len ordS holds
ordS . j = Subst (t,x,(ordP /. j)) ) )
thus ( rng ordS = Support (Subst (t,x,p)) & len ordS = len ordP ) by A2, A6, A11, XBOOLE_0:def 10; :: thesis: for j being Nat st 1 <= j & j <= len ordS holds
ordS . j = Subst (t,x,(ordP /. j))
thus for j being Nat st 1 <= j & j <= len ordS holds
ordS . j = Subst (t,x,(ordP /. j)) by A3, FINSEQ_3:25; :: thesis: verum