let n be Ordinal; :: thesis: for L being non trivial associative commutative well-unital doubleLoopStr
for x being Function of n,L
for b being bag of n
for perm being Permutation of n holds eval (b,x) = eval ((b * perm),(x * perm))
let L be non trivial associative commutative well-unital doubleLoopStr ; :: thesis: for x being Function of n,L
for b being bag of n
for perm being Permutation of n holds eval (b,x) = eval ((b * perm),(x * perm))
let x be Function of n,L; :: thesis: for b being bag of n
for perm being Permutation of n holds eval (b,x) = eval ((b * perm),(x * perm))
let b be bag of n; :: thesis: for perm being Permutation of n holds eval (b,x) = eval ((b * perm),(x * perm))
let perm be Permutation of n; :: thesis: eval (b,x) = eval ((b * perm),(x * perm))
set SG = SgmX ((RelIncl n),(support b));
consider y being FinSequence of L such that
A1: ( len y = len (SgmX ((RelIncl n),(support b))) & eval (b,x) = Product y ) and
A2: for i being Element of NAT st 1 <= i & i <= len y holds
y /. i = (power L) . (((x * (SgmX ((RelIncl n),(support b)))) /. i),((b * (SgmX ((RelIncl n),(support b)))) /. i)) by POLYNOM2:def 2;
A3: RelIncl n linearly_orders support b by PRE_POLY:82;
A4: ( SgmX ((RelIncl n),(support b)) is one-to-one & len (SgmX ((RelIncl n),(support b))) = card (support b) ) by PRE_POLY:10, PRE_POLY:11, PRE_POLY:82;
A5: rng (SgmX ((RelIncl n),(support b))) = support b by A3, PRE_POLY:def 2;
set P = perm " ;
A6: ( dom perm = n & n = rng perm & dom (perm ") = n & n = rng (perm ") ) by FUNCT_2:52, FUNCT_2:def 3;
A7: rng ((perm ") * (SgmX ((RelIncl n),(support b)))) c= support (b * perm)

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng ((perm ") * (SgmX ((RelIncl n),(support b)))) or y in support (b * perm) )
assume A8: y in rng ((perm ") * (SgmX ((RelIncl n),(support b)))) ; :: thesis: y in support (b * perm)
consider w being object such that
A9: ( w in dom ((perm ") * (SgmX ((RelIncl n),(support b)))) & ((perm ") * (SgmX ((RelIncl n),(support b)))) . w = y ) by A8, FUNCT_1:def 3;
A10: ( w in dom (SgmX ((RelIncl n),(support b))) & y = (perm ") . ((SgmX ((RelIncl n),(support b))) . w) & (SgmX ((RelIncl n),(support b))) . w in dom (perm ") ) by A9, FUNCT_1:11, FUNCT_1:12;
then A11: y in rng (perm ") by FUNCT_1:def 3;
A12: (SgmX ((RelIncl n),(support b))) . w = perm . y by A10, FUNCT_1:35, A6;
(SgmX ((RelIncl n),(support b))) . w in support b by A5, A10, FUNCT_1:def 3;
then A13: b . (perm . y) <> 0 by A12, PRE_POLY:def 7;
b . (perm . y) = (b * perm) . y by A11, A6, FUNCT_1:13;
hence y in support (b * perm) by A13, PRE_POLY:def 7; :: thesis: verum

end;

A14: support (b * perm) c= rng ((perm ") * (SgmX ((RelIncl n),(support b))))

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in support (b * perm) or x in rng ((perm ") * (SgmX ((RelIncl n),(support b)))) )
assume A15: x in support (b * perm) ; :: thesis: x in rng ((perm ") * (SgmX ((RelIncl n),(support b))))
A16: (b * perm) . x <> 0 by A15, PRE_POLY:def 7;
then x in dom (b * perm) by FUNCT_1:def 2;
then A17: ( x in dom perm & perm . x in dom b & (b * perm) . x = b . (perm . x) ) by FUNCT_1:11, FUNCT_1:12;
then A18: ( x = (perm ") . (perm . x) & perm . x in support b ) by A16, FUNCT_1:34, PRE_POLY:def 7;
then consider w being object such that
A19: ( w in dom (SgmX ((RelIncl n),(support b))) & (SgmX ((RelIncl n),(support b))) . w = perm . x ) by A5, FUNCT_1:def 3;
( w in dom ((perm ") * (SgmX ((RelIncl n),(support b)))) & ((perm ") * (SgmX ((RelIncl n),(support b)))) . w = (perm ") . ((SgmX ((RelIncl n),(support b))) . w) ) by A6, A17, A19, FUNCT_1:11, FUNCT_1:13;
hence x in rng ((perm ") * (SgmX ((RelIncl n),(support b)))) by A18, A19, FUNCT_1:def 3; :: thesis: verum

end;

reconsider S = (perm ") * (SgmX ((RelIncl n),(support b))) as one-to-one FinSequence of n by A4;
consider Y being FinSequence of L such that
A20: ( len Y = card (support (b * perm)) & eval ((b * perm),(x * perm)) = Product Y ) and
A21: for i being Nat st 1 <= i & i <= len Y holds
Y /. i = (power L) . ((((x * perm) * S) /. i),(((b * perm) * S) /. i)) by Th19, A7, XBOOLE_0:def 10, A14;
A22: len Y = len y by A20, A1, A4, Th2;
for i being Nat st 1 <= i & i <= len Y holds
Y . i = y . i

proof

let i be Nat; :: thesis: ( 1 <= i & i <= len Y implies Y . i = y . i )
assume A23: ( 1 <= i & i <= len Y ) ; :: thesis: Y . i = y . i
A24: rng perm = n by FUNCT_2:def 3;
A25: ( n c= dom x & n = dom b ) by PARTFUN1:def 2;
A26: (x * perm) * S = ((x * perm) * (perm ")) * (SgmX ((RelIncl n),(support b))) by RELAT_1:36
.= (x * (perm * (perm "))) * (SgmX ((RelIncl n),(support b))) by RELAT_1:36
.= (x * (id n)) * (SgmX ((RelIncl n),(support b))) by A24, FUNCT_1:39
.= x * (SgmX ((RelIncl n),(support b))) by A25, RELAT_1:51 ;
A27: (b * perm) * S = ((b * perm) * (perm ")) * (SgmX ((RelIncl n),(support b))) by RELAT_1:36
.= (b * (perm * (perm "))) * (SgmX ((RelIncl n),(support b))) by RELAT_1:36
.= (b * (id n)) * (SgmX ((RelIncl n),(support b))) by A24, FUNCT_1:39
.= b * (SgmX ((RelIncl n),(support b))) by A25, RELAT_1:51 ;
A28: ( i in dom y & i in dom Y ) by A22, A23, FINSEQ_3:25;
hence Y . i = Y /. i by PARTFUN1:def 6
.= (power L) . ((((x * perm) * S) /. i),(((b * perm) * S) /. i)) by A21, A23
.= y /. i by A2, A23, A28, A22, A27, A26
.= y . i by A28, PARTFUN1:def 6 ;
:: thesis: verum

end;

hence eval (b,x) = eval ((b * perm),(x * perm)) by A20, A1, A4, Th2, FINSEQ_1:14; :: thesis: verum