let n be Ordinal; :: thesis: for L being non empty non trivial right_complementable associative commutative add-associative right_zeroed well-unital distributive doubleLoopStr
for b1, b2 being bag of n
for u being set st not u in support b1 & support b2 = (support b1) \/ {u} & ( for u9 being set st u9 <> u holds
b2 . u9 = b1 . u9 ) holds
for x being Function of n,L
for a being Element of L st a = (power L) . (x . u),(b2 . u) holds
eval b2,x = a * (eval b1,x)
let L be non empty non trivial right_complementable associative commutative add-associative right_zeroed well-unital distributive doubleLoopStr ; :: thesis: for b1, b2 being bag of n
for u being set st not u in support b1 & support b2 = (support b1) \/ {u} & ( for u9 being set st u9 <> u holds
b2 . u9 = b1 . u9 ) holds
for x being Function of n,L
for a being Element of L st a = (power L) . (x . u),(b2 . u) holds
eval b2,x = a * (eval b1,x)
let b1, b2 be bag of n; :: thesis: for u being set st not u in support b1 & support b2 = (support b1) \/ {u} & ( for u9 being set st u9 <> u holds
b2 . u9 = b1 . u9 ) holds
for x being Function of n,L
for a being Element of L st a = (power L) . (x . u),(b2 . u) holds
eval b2,x = a * (eval b1,x)
let u be set ; :: thesis: ( not u in support b1 & support b2 = (support b1) \/ {u} & ( for u9 being set st u9 <> u holds
b2 . u9 = b1 . u9 ) implies for x being Function of n,L
for a being Element of L st a = (power L) . (x . u),(b2 . u) holds
eval b2,x = a * (eval b1,x) )
assume that
A1: not u in support b1 and
A2: support b2 = (support b1) \/ {u} and
A3: for u9 being set st u9 <> u holds
b2 . u9 = b1 . u9 ; :: thesis: for x being Function of n,L
for a being Element of L st a = (power L) . (x . u),(b2 . u) holds
eval b2,x = a * (eval b1,x)
u in {u} by TARSKI:def 1;
then A4: u in support b2 by A2, XBOOLE_0:def 3;
set sb2 = SgmX (RelIncl n),(support b2);
set sb1 = SgmX (RelIncl n),(support b1);
let x be Function of n,L; :: thesis: for a being Element of L st a = (power L) . (x . u),(b2 . u) holds
eval b2,x = a * (eval b1,x)
A5: n = dom x by FUNCT_2:def 1;
let a be Element of L; :: thesis: ( a = (power L) . (x . u),(b2 . u) implies eval b2,x = a * (eval b1,x) )
assume A6: a = (power L) . (x . u),(b2 . u) ; :: thesis: eval b2,x = a * (eval b1,x)
RelIncl n linearly_orders support b2 by Th15;
then u in rng (SgmX (RelIncl n),(support b2)) by A4, PRE_POLY:def 2;
then consider k being Nat such that
A7: k in dom (SgmX (RelIncl n),(support b2)) and
A8: (SgmX (RelIncl n),(support b2)) . k = u by FINSEQ_2:11;
A9: (SgmX (RelIncl n),(support b2)) /. k = u by A7, A8, PARTFUN1:def 8;
reconsider u = u as Element of n by A4;
A10: dom (SgmX (RelIncl n),(support b2)) = Seg (len (SgmX (RelIncl n),(support b2))) by FINSEQ_1:def 3;
then A11: k <= len (SgmX (RelIncl n),(support b2)) by A7, FINSEQ_1:3;
A12: 1 <= k by A7, A10, FINSEQ_1:3;
then 1 - 1 <= k - 1 by XREAL_1:11;
then reconsider k9 = k - 1 as Element of NAT by INT_1:16;
A13: k9 + 1 = k + 0 ;
A14: RelIncl n linearly_orders support b1 by Th15;

per cases ( n = {} or n <> {} ) ;

suppose A15: n = {} ; :: thesis: eval b2,x = a * (eval b1,x)

A16: b2 in Bags n by PRE_POLY:def 12;
u in {u} by TARSKI:def 1;
then u in support b2 by A2, XBOOLE_0:def 3;
then A17: b2 . u <> 0 by PRE_POLY:def 7;
Bags n = {(EmptyBag n)} by A15, PRE_POLY:51, TARSKI:def 1;
then b2 = EmptyBag n by A16, TARSKI:def 1;
hence eval b2,x = a * (eval b1,x) by A17, PRE_POLY:52; :: thesis: verum

end;

suppose n <> {} ; :: thesis: eval b2,x = a * (eval b1,x)

then reconsider n9 = n as non empty Ordinal ;
reconsider x9 = x as Function of n9,L ;
reconsider b1 = b1, b2 = b2 as bag of n9 ;
reconsider sb2 = SgmX (RelIncl n),(support b2), sb1 = SgmX (RelIncl n),(support b1) as FinSequence of n9 ;
reconsider u = u as Element of n9 ;
consider yb2 being FinSequence of the carrier of L such that
A18: len yb2 = len sb2 and
A19: eval b2,x9 = Product yb2 and
A20: for i being Element of NAT st 1 <= i & i <= len yb2 holds
yb2 /. i = (power L) . ((x * sb2) /. i),((b2 * sb2) /. i) by Def2;
consider yb1 being FinSequence of the carrier of L such that
A21: len yb1 = len sb1 and
A22: eval b1,x9 = Product yb1 and
A23: for i being Element of NAT st 1 <= i & i <= len yb1 holds
yb1 /. i = (power L) . ((x * sb1) /. i),((b1 * sb1) /. i) by Def2;
set ytmp = Ins yb1,k9,a;
A24: (len sb1) + 1 = (card (support b1)) + 1 by Th15, PRE_POLY:11
.= card (support b2) by A1, A2, CARD_2:54
.= len sb2 by Th15, PRE_POLY:11 ;
then A25: len yb2 = len (Ins yb1,k9,a) by A18, A21, FINSEQ_5:72;
A26: sb2 = Ins sb1,k9,u by A1, A2, A7, A9, A13, Th13, Th15;
A27: for i being Nat st 1 <= i & i <= len yb2 holds
yb2 . i = (Ins yb1,k9,a) . i

proof

let i be Nat; :: thesis: ( 1 <= i & i <= len yb2 implies yb2 . i = (Ins yb1,k9,a) . i )
assume that
A28: 1 <= i and
A29: i <= len yb2 ; :: thesis: yb2 . i = (Ins yb1,k9,a) . i
A30: i in Seg (len yb2) by A28, A29, FINSEQ_1:3;
then A31: yb2 /. i = (power L) . ((x * (Ins sb1,k9,u)) /. i),((b2 * (Ins sb1,k9,u)) /. i) by A26, A20, A28, A29;
A32: i in dom yb2 by A30, FINSEQ_1:def 3;
i in Seg (len (Ins yb1,k9,a)) by A25, A28, A29, FINSEQ_1:3;
then A33: i in dom (Ins yb1,k9,a) by FINSEQ_1:def 3;
A34: 1 - 1 <= i - 1 by A28, XREAL_1:11;
then A35: i - 1 is Element of NAT by INT_1:16;

now

per cases ( i = k or i <> k ) ;

case A36: i = k ; :: thesis: (Ins yb1,k9,a) . i = yb2 . i

A37: sb2 . k in {u} by A8, TARSKI:def 1;
then A38: k in dom (x * sb2) by A5, A7, A8, FUNCT_1:21;
then A39: (x * sb2) /. k = (x * sb2) . k by PARTFUN1:def 8
.= x . u by A8, A38, FUNCT_1:22 ;
A40: support b2 c= dom b2 by PRE_POLY:37;
sb2 . k in support b2 by A2, A37, XBOOLE_0:def 3;
then A41: k in dom (b2 * sb2) by A7, A40, FUNCT_1:21;
then (b2 * sb2) /. k = (b2 * sb2) . k by PARTFUN1:def 8
.= b2 . u by A8, A41, FUNCT_1:22 ;
then A42: yb2 /. i = (power L) . (x . u),(b2 . u) by A20, A28, A29, A30, A36, A39;
A43: k9 <= len yb1 by A13, A18, A21, A24, A29, A36, XREAL_1:8;
thus (Ins yb1,k9,a) . i = (Ins yb1,k9,a) /. i by A33, PARTFUN1:def 8
.= yb2 /. i by A6, A13, A36, A43, A42, FINSEQ_5:76
.= yb2 . i by A32, PARTFUN1:def 8 ; :: thesis: verum

end;

case A44: i <> k ; :: thesis: yb2 . i = (Ins yb1,k9,a) . i

len (Ins sb1,k9,u) = (len sb1) + 1 by FINSEQ_5:72;
then A45: dom (Ins sb1,k9,u) = Seg ((len sb1) + 1) by FINSEQ_1:def 3;

now

per cases ( i < k or i > k ) by A44, XXREAL_0:1;

case A46: i < k ; :: thesis: yb2 . i = (Ins yb1,k9,a) . i

then A47: i <= k9 by A13, NAT_1:13;
then A48: i in Seg k9 by A28, FINSEQ_1:3;
A49: yb1 | (Seg k9) is FinSequence by FINSEQ_1:19;
k9 <= len yb1 by A11, A13, A21, A24, XREAL_1:8;
then i in dom (yb1 | (Seg k9)) by A48, A49, FINSEQ_1:21;
then A50: i in dom (yb1 | k9) by FINSEQ_1:def 15;
A51: sb1 | (Seg k9) is FinSequence by FINSEQ_1:19;
A52: rng sb1 c= n by FINSEQ_1:def 4;
A53: i < len yb2 by A11, A18, A46, XXREAL_0:2;
then A54: i <= len yb1 by A18, A21, A24, NAT_1:13;
i <= len sb1 by A18, A24, A53, NAT_1:13;
then i in Seg (len sb1) by A28, FINSEQ_1:3;
then A55: i in dom sb1 by FINSEQ_1:def 3;
then A56: sb1 . i in rng sb1 by FUNCT_1:def 5;
then A57: i in dom (x * sb1) by A5, A55, A52, FUNCT_1:21;

A58: now

assume sb1 /. i = u ; :: thesis: contradiction
then sb1 . i = u by A55, PARTFUN1:def 8;
then u in rng sb1 by A55, FUNCT_1:def 5;
hence contradiction by A1, A14, PRE_POLY:def 2; :: thesis: verum

end;

A59: k - 1 <= ((len sb1) + 1) - 1 by A11, A24, XREAL_1:11;
A60: rng (Ins sb1,k9,u) c= n by FINSEQ_1:def 4;
sb1 . i in n by A56, A52;
then sb1 . i in dom b1 by PARTFUN1:def 4;
then A61: i in dom (b1 * sb1) by A55, FUNCT_1:21;
i in Seg k9 by A28, A47, FINSEQ_1:3;
then i in dom (sb1 | (Seg k9)) by A59, A51, FINSEQ_1:21;
then A62: i in dom (sb1 | k9) by FINSEQ_1:def 15;
i <= (len sb1) + 1 by A11, A24, A46, XXREAL_0:2;
then A63: i in dom (Ins sb1,k9,u) by A28, A45, FINSEQ_1:3;
then A64: (Ins sb1,k9,u) . i in rng (Ins sb1,k9,u) by FUNCT_1:def 5;
then A65: i in dom (x * (Ins sb1,k9,u)) by A5, A63, A60, FUNCT_1:21;
then A66: (x * (Ins sb1,k9,u)) /. i = (x * (Ins sb1,k9,u)) . i by PARTFUN1:def 8
.= x . ((Ins sb1,k9,u) . i) by A65, FUNCT_1:22
.= x . ((Ins sb1,k9,u) /. i) by A63, PARTFUN1:def 8
.= x . (sb1 /. i) by A62, FINSEQ_5:75
.= x . (sb1 . i) by A55, PARTFUN1:def 8
.= (x * sb1) . i by A57, FUNCT_1:22
.= (x * sb1) /. i by A57, PARTFUN1:def 8 ;
dom b2 = n by PARTFUN1:def 4;
then A67: i in dom (b2 * (Ins sb1,k9,u)) by A63, A64, A60, FUNCT_1:21;
then (b2 * (Ins sb1,k9,u)) /. i = (b2 * (Ins sb1,k9,u)) . i by PARTFUN1:def 8
.= b2 . ((Ins sb1,k9,u) . i) by A67, FUNCT_1:22
.= b2 . ((Ins sb1,k9,u) /. i) by A63, PARTFUN1:def 8
.= b2 . (sb1 /. i) by A62, FINSEQ_5:75
.= b1 . (sb1 /. i) by A3, A58
.= b1 . (sb1 . i) by A55, PARTFUN1:def 8
.= (b1 * sb1) . i by A61, FUNCT_1:22
.= (b1 * sb1) /. i by A61, PARTFUN1:def 8 ;
then A68: yb2 /. i = yb1 /. i by A23, A28, A30, A31, A54, A66
.= (Ins yb1,k9,a) /. i by A50, FINSEQ_5:75 ;
thus yb2 . i = yb2 /. i by A32, PARTFUN1:def 8
.= (Ins yb1,k9,a) . i by A33, A68, PARTFUN1:def 8 ; :: thesis: verum

end;

case A69: i > k ; :: thesis: yb2 . i = (Ins yb1,k9,a) . i

reconsider i1 = i - 1 as Element of NAT by A34, INT_1:16;
A70: (i - 1) + 1 = i + 0 ;
A71: rng sb1 c= n by FINSEQ_1:def 4;
A72: i - 1 <= (len sb2) - 1 by A18, A29, XREAL_1:11;
1 < i by A12, A69, XXREAL_0:2;
then A73: 1 <= i - 1 by A35, A70, NAT_1:13;
then i1 in Seg (len sb1) by A24, A72, FINSEQ_1:3;
then A74: i1 in dom sb1 by FINSEQ_1:def 3;
then A75: sb1 . i1 in rng sb1 by FUNCT_1:def 5;
then A76: i1 in dom (x * sb1) by A5, A74, A71, FUNCT_1:21;
dom b1 = n by PARTFUN1:def 4;
then A77: i1 in dom (b1 * sb1) by A74, A75, A71, FUNCT_1:21;

A78: now

assume sb1 /. i1 = u ; :: thesis: contradiction
then sb1 . i1 = u by A74, PARTFUN1:def 8;
then u in rng sb1 by A74, FUNCT_1:def 5;
hence contradiction by A1, A14, PRE_POLY:def 2; :: thesis: verum

end;

A79: i = i1 + 1 ;
A80: rng (Ins sb1,k9,u) c= n by FINSEQ_1:def 4;
A81: i1 + 1 = i + 0 ;
then A82: k9 + 1 <= i1 by A69, NAT_1:13;
A83: i in dom (Ins sb1,k9,u) by A18, A24, A28, A29, A45, FINSEQ_1:3;
then A84: (Ins sb1,k9,u) . i in rng (Ins sb1,k9,u) by FUNCT_1:def 5;
then A85: i in dom (x * (Ins sb1,k9,u)) by A5, A83, A80, FUNCT_1:21;
then A86: (x * (Ins sb1,k9,u)) /. i = (x * (Ins sb1,k9,u)) . i by PARTFUN1:def 8
.= x . ((Ins sb1,k9,u) . i) by A85, FUNCT_1:22
.= x . ((Ins sb1,k9,u) /. i) by A83, PARTFUN1:def 8
.= x . (sb1 /. i1) by A24, A72, A81, A82, FINSEQ_5:77
.= x . (sb1 . i1) by A74, PARTFUN1:def 8
.= (x * sb1) . i1 by A76, FUNCT_1:22
.= (x * sb1) /. i1 by A76, PARTFUN1:def 8 ;
dom b2 = n by PARTFUN1:def 4;
then A87: i in dom (b2 * (Ins sb1,k9,u)) by A83, A84, A80, FUNCT_1:21;
then (b2 * (Ins sb1,k9,u)) /. i = (b2 * (Ins sb1,k9,u)) . i by PARTFUN1:def 8
.= b2 . ((Ins sb1,k9,u) . i) by A87, FUNCT_1:22
.= b2 . ((Ins sb1,k9,u) /. i) by A83, PARTFUN1:def 8
.= b2 . (sb1 /. i1) by A24, A72, A81, A82, FINSEQ_5:77
.= b1 . (sb1 /. i1) by A3, A78
.= b1 . (sb1 . i1) by A74, PARTFUN1:def 8
.= (b1 * sb1) . i1 by A77, FUNCT_1:22
.= (b1 * sb1) /. i1 by A77, PARTFUN1:def 8 ;
then A88: yb2 /. i = yb1 /. i1 by A21, A23, A24, A31, A73, A72, A86
.= (Ins yb1,k9,a) /. i by A21, A24, A72, A79, A82, FINSEQ_5:77 ;
thus yb2 . i = yb2 /. i by A32, PARTFUN1:def 8
.= (Ins yb1,k9,a) . i by A33, A88, PARTFUN1:def 8 ; :: thesis: verum

end;

end;

end;

hence yb2 . i = (Ins yb1,k9,a) . i ; :: thesis: verum

end;

end;

end;

hence yb2 . i = (Ins yb1,k9,a) . i ; :: thesis: verum

end;

Product (((yb1 | k9) ^ <*a*>) ^ (yb1 /^ k9)) = (Product ((yb1 | k9) ^ <*a*>)) * (Product (yb1 /^ k9)) by GROUP_4:8
.= ((Product (yb1 | k9)) * (Product <*a*>)) * (Product (yb1 /^ k9)) by GROUP_4:8
.= ((Product (yb1 | k9)) * (Product (yb1 /^ k9))) * (Product <*a*>) by GROUP_1:def 4
.= (Product ((yb1 | k9) ^ (yb1 /^ k9))) * (Product <*a*>) by GROUP_4:8
.= (Product yb1) * (Product <*a*>) by RFINSEQ:21
.= (eval b1,x9) * a by A22, GROUP_4:12 ;
then Product (Ins yb1,k9,a) = (eval b1,x9) * a by FINSEQ_5:def 4;
hence eval b2,x = a * (eval b1,x) by A19, A25, A27, FINSEQ_1:18; :: thesis: verum

end;

end;