let n be Ordinal; :: thesis: for L being non empty non trivial right_complementable associative commutative Abelian add-associative right_zeroed well-unital distributive doubleLoopStr
for x being Function of n,L
for b being bag of n
for i being object
for j being Nat st i in n holds
(eval ((b +* (i,j)),x)) * ((power L) . ((x /. i),(b . i))) = (eval (b,x)) * ((power L) . ((x /. i),j))
let L be non empty non trivial right_complementable associative commutative Abelian add-associative right_zeroed well-unital distributive doubleLoopStr ; :: thesis: for x being Function of n,L
for b being bag of n
for i being object
for j being Nat st i in n holds
(eval ((b +* (i,j)),x)) * ((power L) . ((x /. i),(b . i))) = (eval (b,x)) * ((power L) . ((x /. i),j))
let x be Function of n,L; :: thesis: for b being bag of n
for i being object
for j being Nat st i in n holds
(eval ((b +* (i,j)),x)) * ((power L) . ((x /. i),(b . i))) = (eval (b,x)) * ((power L) . ((x /. i),j))
set E = EmptyBag n;
let b be bag of n; :: thesis: for i being object
for j being Nat st i in n holds
(eval ((b +* (i,j)),x)) * ((power L) . ((x /. i),(b . i))) = (eval (b,x)) * ((power L) . ((x /. i),j))
let i be object ; :: thesis: for j being Nat st i in n holds
(eval ((b +* (i,j)),x)) * ((power L) . ((x /. i),(b . i))) = (eval (b,x)) * ((power L) . ((x /. i),j))
let j be Nat; :: thesis: ( i in n implies (eval ((b +* (i,j)),x)) * ((power L) . ((x /. i),(b . i))) = (eval (b,x)) * ((power L) . ((x /. i),j)) )
assume A1: i in n ; :: thesis: (eval ((b +* (i,j)),x)) * ((power L) . ((x /. i),(b . i))) = (eval (b,x)) * ((power L) . ((x /. i),j))
A2: i is set by TARSKI:1;
set d = b +* (i,j);
b +* (i,j) = ((b +* (i,j)) +* (i,0)) + ((EmptyBag n) +* (i,((b +* (i,j)) . i))) by Th15;
then b +* (i,j) = (b +* (i,0)) + ((EmptyBag n) +* (i,((b +* (i,j)) . i))) by A2, FUNCT_7:34;
then A3: (eval ((b +* (i,j)),x)) * ((power L) . ((x /. i),(b . i))) = ((eval ((b +* (i,0)),x)) * (eval (((EmptyBag n) +* (i,((b +* (i,j)) . i))),x))) * ((power L) . ((x /. i),(b . i))) by POLYNOM2:16;
( dom b = n & n = dom x ) by PARTFUN1:def 2;
then A5: ( (b +* (i,j)) . i = j & x /. i = x . i ) by A1, FUNCT_7:31, PARTFUN1:def 6;
A10: b = (b +* (i,0)) + ((EmptyBag n) +* (i,(b . i))) by Th15;
(power L) . ((x /. i),(b . i)) = eval (((EmptyBag n) +* (i,(b . i))),x) by A5, Th14, A1;
then A14: (eval ((b +* (i,0)),x)) * ((power L) . ((x /. i),(b . i))) = eval (b,x) by POLYNOM2:16, A10;
thus (eval ((b +* (i,j)),x)) * ((power L) . ((x /. i),(b . i))) = ((eval ((b +* (i,0)),x)) * ((power L) . ((x /. i),(b . i)))) * (eval (((EmptyBag n) +* (i,j)),x)) by A5, A3, GROUP_1:def 3
.= (eval (b,x)) * ((power L) . ((x /. i),j)) by A14, A5, A1, Th14 ; :: thesis: verum