let O be Ordinal; :: thesis: for L being non trivial right_complementable associative commutative Abelian add-associative right_zeroed well-unital distributive doubleLoopStr
for p being Polynomial of O,L
for x being Function of O,L
for perm being Permutation of O holds eval (p,x) = eval ((p permuted_by perm),(x * (perm ")))
let L be non trivial right_complementable associative commutative Abelian add-associative right_zeroed well-unital distributive doubleLoopStr ; :: thesis: for p being Polynomial of O,L
for x being Function of O,L
for perm being Permutation of O holds eval (p,x) = eval ((p permuted_by perm),(x * (perm ")))
let p be Polynomial of O,L; :: thesis: for x being Function of O,L
for perm being Permutation of O holds eval (p,x) = eval ((p permuted_by perm),(x * (perm ")))
let x be Function of O,L; :: thesis: for perm being Permutation of O holds eval (p,x) = eval ((p permuted_by perm),(x * (perm ")))
let perm be Permutation of O; :: thesis: eval (p,x) = eval ((p permuted_by perm),(x * (perm ")))
set SB = SgmX ((BagOrder O),(Support p));
consider y being FinSequence of L such that
A1: ( len y = len (SgmX ((BagOrder O),(Support p))) & eval (p,x) = Sum y ) and
A2: for i being Element of NAT st 1 <= i & i <= len y holds
y /. i = ((p * (SgmX ((BagOrder O),(Support p)))) /. i) * (eval (((SgmX ((BagOrder O),(Support p))) /. i),x)) by POLYNOM2:def 4;
A3: BagOrder O linearly_orders Support p by POLYNOM2:18;
A4: ( SgmX ((BagOrder O),(Support p)) is one-to-one & len (SgmX ((BagOrder O),(Support p))) = card (Support p) ) by PRE_POLY:10, PRE_POLY:11, POLYNOM2:18;
A5: rng (SgmX ((BagOrder O),(Support p))) = Support p by A3, PRE_POLY:def 2;
set P = p permuted_by perm;
defpred S1[ bag of O, bag of O] means $2 = $1 * (perm ");
A6: for x being Element of Bags O ex y being Element of Bags O st S1[x,y]
proof
let x be Element of Bags O; :: thesis: ex y being Element of Bags O st S1[x,y]
x * (perm ") in Bags O by PRE_POLY:def 12;
hence ex y being Element of Bags O st S1[x,y] ; :: thesis: verum
end;
consider f being Function of (Bags O),(Bags O) such that
A7: for x being Element of Bags O holds S1[x,f . x] from FUNCT_2:sch 3(A6);
 A8: dom f = Bags O by FUNCT_2:52;
( rng perm = O & O = dom perm ) by FUNCT_2:52, FUNCT_2:def 3;
then A9: ( perm * (perm ") = id O & id O = (perm ") * perm ) by FUNCT_1:39;
A10: f is one-to-one
proof
let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in dom f or not x2 in dom f or not f . x1 = f . x2 or x1 = x2 )
assume A11: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 ) ; :: thesis: x1 = x2
reconsider x1 = x1, x2 = x2 as Element of Bags O by A11;
A12: ( f . x1 = x1 * (perm ") & f . x2 = x2 * (perm ") ) by A7;
A13: ( dom x1 = O & O = dom x2 ) by PARTFUN1:def 2;
A14: (x1 * (perm ")) * perm = x1 * (id O) by A9, RELAT_1:36
.= x1 by A13, RELAT_1:51 ;
(x2 * (perm ")) * perm = x2 * (id O) by A9, RELAT_1:36
.= x2 by A13, RELAT_1:51 ;
hence x1 = x2 by A11, A12, A14; :: thesis: verum
end;
reconsider fSB = f * (SgmX ((BagOrder O),(Support p))) as one-to-one FinSequence of Bags O by A4, A10;
rng (SgmX ((BagOrder O),(Support p))) c= dom f by A8;
then A15: dom fSB = dom (SgmX ((BagOrder O),(Support p))) by RELAT_1:27;
A16: rng fSB c= Support (p permuted_by perm)
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng fSB or y in Support (p permuted_by perm) )
assume A17: y in rng fSB ; :: thesis: y in Support (p permuted_by perm)
consider x being object such that
A18: ( x in dom fSB & fSB . x = y ) by FUNCT_1:def 3, A17;
A19: ( y = f . ((SgmX ((BagOrder O),(Support p))) . x) & x in dom (SgmX ((BagOrder O),(Support p))) & (SgmX ((BagOrder O),(Support p))) . x in dom f ) by A18, FUNCT_1:11, FUNCT_1:12;
then reconsider SBx = (SgmX ((BagOrder O),(Support p))) . x as Element of Bags O ;
SBx in Support p by A19, A5, FUNCT_1:def 3;
then SBx * (perm ") in Support (p permuted_by perm) by Th22;
hence y in Support (p permuted_by perm) by A7, A19; :: thesis: verum
end;
Support (p permuted_by perm) c= rng fSB
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Support (p permuted_by perm) or y in rng fSB )
assume A20: y in Support (p permuted_by perm) ; :: thesis: y in rng fSB
reconsider y = y as Element of Bags O by A20;
A21: dom y = O by PARTFUN1:def 2;
A22: y * perm in Support p by A20, Th21;
then A23: f . (y * perm) = (y * perm) * (perm ") by A7
.= y * (id O) by A9, RELAT_1:36
.= y by A21, RELAT_1:51 ;
consider w being object such that
A24: ( w in dom (SgmX ((BagOrder O),(Support p))) & (SgmX ((BagOrder O),(Support p))) . w = y * perm ) by A5, A22, FUNCT_1:def 3;
( w in dom fSB & fSB . w = y ) by A8, A22, A23, A24, FUNCT_1:11, FUNCT_1:13;
hence y in rng fSB by FUNCT_1:def 3; :: thesis: verum
end;
then consider z being FinSequence of L such that
A25: ( len z = card (Support (p permuted_by perm)) & eval ((p permuted_by perm),(x * (perm "))) = Sum z ) and
A26: for i being Nat st 1 <= i & i <= len z holds
z /. i = (((p permuted_by perm) * fSB) /. i) * (eval ((fSB /. i),(x * (perm ")))) by A16, XBOOLE_0:def 10, Th24;
A27: len y = len z by A1, A4, A25, Th23;
for i being Nat st 1 <= i & i <= len y holds
y . i = z . i
proof
let i be Nat; :: thesis: ( 1 <= i & i <= len y implies y . i = z . i )
assume A28: ( 1 <= i & i <= len y ) ; :: thesis: y . i = z . i
A29: i in NAT by ORDINAL1:def 12;
A30: ( i in dom y & i in dom z & i in dom (SgmX ((BagOrder O),(Support p))) ) by A28, A1, FINSEQ_3:25, A27;
then A31: (SgmX ((BagOrder O),(Support p))) . i = (SgmX ((BagOrder O),(Support p))) /. i by PARTFUN1:def 6;
then reconsider SBi = (SgmX ((BagOrder O),(Support p))) . i as Element of Bags O ;
A32: dom SBi = O by PARTFUN1:def 2;
A33: (SBi * (perm ")) * perm = SBi * (id O) by A9, RELAT_1:36
.= SBi by A32, RELAT_1:51 ;
( dom p = Bags O & Bags O = dom (p permuted_by perm) ) by FUNCT_2:def 1;
then ( rng (SgmX ((BagOrder O),(Support p))) c= dom p & rng fSB c= dom (p permuted_by perm) ) ;
then A34: ( dom (p * (SgmX ((BagOrder O),(Support p)))) = dom (SgmX ((BagOrder O),(Support p))) & dom ((p permuted_by perm) * fSB) = dom fSB ) by RELAT_1:27;
then A35: ((p permuted_by perm) * fSB) /. i = ((p permuted_by perm) * fSB) . i by A15, A28, FINSEQ_3:25, A1, PARTFUN1:def 6
.= (p permuted_by perm) . (fSB . i) by A1, A15, A28, FINSEQ_3:25, A34, FUNCT_1:12
.= (p permuted_by perm) . (f . SBi) by A15, A28, FINSEQ_3:25, A1, FUNCT_1:12
.= (p permuted_by perm) . (SBi * (perm ")) by A7
.= p . ((SBi * (perm ")) * perm) by Def4
.= (p * (SgmX ((BagOrder O),(Support p)))) . i by A28, A1, A33, FINSEQ_3:25, A34, FUNCT_1:12
.= (p * (SgmX ((BagOrder O),(Support p)))) /. i by A34, A28, A1, FINSEQ_3:25, PARTFUN1:def 6 ;
A36: ((SgmX ((BagOrder O),(Support p))) /. i) * (perm ") = f . SBi by A7, A31
.= fSB . i by A15, A28, A1, FINSEQ_3:25, FUNCT_1:12
.= fSB /. i by A15, A28, A1, FINSEQ_3:25, PARTFUN1:def 6 ;
thus y . i = y /. i by A30, PARTFUN1:def 6
.= ((p * (SgmX ((BagOrder O),(Support p)))) /. i) * (eval (((SgmX ((BagOrder O),(Support p))) /. i),x)) by A29, A2, A28
.= (((p permuted_by perm) * fSB) /. i) * (eval ((fSB /. i),(x * (perm ")))) by A35, A36, Th20
.= z /. i by A26, A28, A27
.= z . i by A30, PARTFUN1:def 6 ; :: thesis: verum
end;
hence eval (p,x) = eval ((p permuted_by perm),(x * (perm "))) by FINSEQ_1:14, A1, A4, A25, Th23; :: thesis: verum