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 object st not u in support b1 & support b2 = (support b1) \/ {u} & ( for u9 being object 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 trivial right_complementable associative commutative add-associative right_zeroed well-unital distributive doubleLoopStr ; :: thesis: for b1, b2 being bag of n
for u being object st not u in support b1 & support b2 = (support b1) \/ {u} & ( for u9 being object 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 object st not u in support b1 & support b2 = (support b1) \/ {u} & ( for u9 being object 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 object ; :: thesis: ( not u in support b1 & support b2 = (support b1) \/ {u} & ( for u9 being object 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 object 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 PRE_POLY:82;
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:10;
A9: (SgmX ((RelIncl n),(support b2))) /. k = u by A7, A8, PARTFUN1:def 6;
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;
A11: k <= len (SgmX ((RelIncl n),(support b2))) by A7, FINSEQ_3:25;
A12: 1 <= k by A7, A10, FINSEQ_1:1;
then 1 - 1 <= k - 1 by XREAL_1:9;
then reconsider k9 = k - 1 as Element of NAT by INT_1:3;
A13: k9 + 1 = k + 0 ;
A14: RelIncl n linearly_orders support b1 by PRE_POLY:82;

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;
then b2 = EmptyBag n by A16, TARSKI:def 1;
hence eval (b2,x) = a * (eval (b1,x)) by A17; :: 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 Def1;
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 Def1;
set ytmp = Ins (yb1,k9,a);
A24: (len sb1) + 1 = (card (support b1)) + 1 by PRE_POLY:11, PRE_POLY:82
.= card (support b2) by A1, A2, CARD_2:41
.= len sb2 by PRE_POLY:11, PRE_POLY:82 ;
then A25: len yb2 = len (Ins (yb1,k9,a)) by A18, A21, FINSEQ_5:69;
A26: sb2 = Ins (sb1,k9,u) by A1, A2, A7, A9, A13, PRE_POLY:80, PRE_POLY:82;
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:1;
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:1;
then A33: i in dom (Ins (yb1,k9,a)) by FINSEQ_1:def 3;
A34: 1 - 1 <= i - 1 by A28, XREAL_1:9;
then A35: i - 1 is Element of NAT by INT_1:3;

now :: thesis: ( ( i = k & (Ins (yb1,k9,a)) . i = yb2 . i ) or ( i <> k & yb2 . i = (Ins (yb1,k9,a)) . i ) )

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:11;
then A39: (x * sb2) /. k = (x * sb2) . k by PARTFUN1:def 6
.= x . u by A8, A38, FUNCT_1:12 ;
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:11;
then (b2 * sb2) /. k = (b2 * sb2) . k by PARTFUN1:def 6
.= b2 . u by A8, A41, FUNCT_1:12 ;
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:6;
yb2 . i = yb2 /. i by PARTFUN1:def 6, A32;
hence (Ins (yb1,k9,a)) . i = yb2 . i by A6, A13, A36, A43, A42, FINSEQ_5:73; :: 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:69;
then A45: dom (Ins (sb1,k9,u)) = Seg ((len sb1) + 1) by FINSEQ_1:def 3;

now :: thesis: ( ( i < k & yb2 . i = (Ins (yb1,k9,a)) . i ) or ( i > k & yb2 . i = (Ins (yb1,k9,a)) . i ) )

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:1;
A49: yb1 | (Seg k9) is FinSequence by FINSEQ_1:15;
k9 <= len yb1 by A11, A13, A21, A24, XREAL_1:6;
then W: i in dom (yb1 | (Seg k9)) by A48, A49, FINSEQ_1:17;
then A50: i in dom (yb1 | k9) by FINSEQ_1:def 16;
A51: sb1 | (Seg k9) is FinSequence by FINSEQ_1:15;
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;
ST: i in dom yb1 by W, RELAT_1:57;
i <= len sb1 by A18, A24, A53, NAT_1:13;
then A55: i in dom sb1 by FINSEQ_3:25, A28;
then A56: sb1 . i in rng sb1 by FUNCT_1:def 3;
then A57: i in dom (x * sb1) by A5, A55, A52, FUNCT_1:11;

A58: now :: thesis: not sb1 . i = u

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

end;

A59: k - 1 <= ((len sb1) + 1) - 1 by A11, A24, XREAL_1:9;
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 2;
then A61: i in dom (b1 * sb1) by A55, FUNCT_1:11;
i in Seg k9 by A28, A47, FINSEQ_1:1;
then i in dom (sb1 | (Seg k9)) by A59, A51, FINSEQ_1:17;
then A62: i in dom (sb1 | k9) by FINSEQ_1:def 16;
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:1;
then A64: (Ins (sb1,k9,u)) . i in rng (Ins (sb1,k9,u)) by FUNCT_1:def 3;
then A65: i in dom (x * (Ins (sb1,k9,u))) by A5, A63, A60, FUNCT_1:11;
then A66: (x * (Ins (sb1,k9,u))) /. i = (x * (Ins (sb1,k9,u))) . i by PARTFUN1:def 6
.= x . ((Ins (sb1,k9,u)) . i) by A65, FUNCT_1:12
.= x . (sb1 . i) by A62, FINSEQ_5:72
.= (x * sb1) . i by A57, FUNCT_1:12
.= (x * sb1) /. i by A57, PARTFUN1:def 6 ;
dom b2 = n by PARTFUN1:def 2;
then A67: i in dom (b2 * (Ins (sb1,k9,u))) by A63, A64, A60, FUNCT_1:11;
then (b2 * (Ins (sb1,k9,u))) /. i = (b2 * (Ins (sb1,k9,u))) . i by PARTFUN1:def 6
.= b2 . ((Ins (sb1,k9,u)) . i) by A67, FUNCT_1:12
.= b2 . (sb1 . i) by A62, FINSEQ_5:72
.= b1 . (sb1 . i) by A3, A58
.= (b1 * sb1) . i by A61, FUNCT_1:12
.= (b1 * sb1) /. i by A61, PARTFUN1:def 6 ;
then A68: yb2 /. i = yb1 /. i by A23, A28, A30, A31, A54, A66
.= yb1 . i by PARTFUN1:def 6, ST
.= (Ins (yb1,k9,a)) . i by A50, FINSEQ_5:72
.= (Ins (yb1,k9,a)) /. i by A33, PARTFUN1:def 6 ;
thus yb2 . i = yb2 /. i by A32, PARTFUN1:def 6
.= (Ins (yb1,k9,a)) . i by A33, A68, PARTFUN1:def 6 ; :: 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:3;
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:9;
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:1;
then A74: i1 in dom sb1 by FINSEQ_1:def 3;
then A75: sb1 . i1 in rng sb1 by FUNCT_1:def 3;
then A76: i1 in dom (x * sb1) by A5, A74, A71, FUNCT_1:11;
dom b1 = n by PARTFUN1:def 2;
then A77: i1 in dom (b1 * sb1) by A74, A75, A71, FUNCT_1:11;

A78: now :: thesis: not sb1 /. i1 = u

assume sb1 /. i1 = u ; :: thesis: contradiction
then sb1 . i1 = u by A74, PARTFUN1:def 6;
then u in rng sb1 by A74, FUNCT_1:def 3;
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:1;
then A84: (Ins (sb1,k9,u)) . i in rng (Ins (sb1,k9,u)) by FUNCT_1:def 3;
then A85: i in dom (x * (Ins (sb1,k9,u))) by A5, A83, A80, FUNCT_1:11;
then A86: (x * (Ins (sb1,k9,u))) /. i = (x * (Ins (sb1,k9,u))) . i by PARTFUN1:def 6
.= x . ((Ins (sb1,k9,u)) . i) by A85, FUNCT_1:12
.= x . (sb1 . i1) by A24, A72, A81, A82, FINSEQ_5:74
.= (x * sb1) . i1 by A76, FUNCT_1:12
.= (x * sb1) /. i1 by A76, PARTFUN1:def 6 ;
W1: 1 <= i1 by A73;
i1 <= len sb1 by A74, FINSEQ_3:25;
then i1 <= len yb1 by A21;
then Ze: i1 in dom yb1 by W1, FINSEQ_3:25;
dom b2 = n by PARTFUN1:def 2;
then A87: i in dom (b2 * (Ins (sb1,k9,u))) by A83, A84, A80, FUNCT_1:11;
then (b2 * (Ins (sb1,k9,u))) /. i = (b2 * (Ins (sb1,k9,u))) . i by PARTFUN1:def 6
.= b2 . ((Ins (sb1,k9,u)) . i) by A87, FUNCT_1:12
.= b2 . (sb1 . i1) by A24, A72, A81, A82, FINSEQ_5:74
.= b2 . (sb1 /. i1) by A74, PARTFUN1:def 6
.= b1 . (sb1 /. i1) by A3, A78
.= b1 . (sb1 . i1) by A74, PARTFUN1:def 6
.= (b1 * sb1) . i1 by A77, FUNCT_1:12
.= (b1 * sb1) /. i1 by A77, PARTFUN1:def 6 ;
then A88: yb2 /. i = yb1 /. i1 by A21, A23, A24, A31, A73, A72, A86
.= yb1 . i1 by Ze, PARTFUN1:def 6
.= (Ins (yb1,k9,a)) . i by A21, A24, A72, A79, A82, FINSEQ_5:74
.= (Ins (yb1,k9,a)) /. i by A33, PARTFUN1:def 6 ;
thus yb2 . i = yb2 /. i by A32, PARTFUN1:def 6
.= (Ins (yb1,k9,a)) . i by A33, A88, PARTFUN1:def 6 ; :: 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:5
.= ((Product (yb1 | k9)) * (Product <*a*>)) * (Product (yb1 /^ k9)) by GROUP_4:5
.= ((Product (yb1 | k9)) * (Product (yb1 /^ k9))) * (Product <*a*>) by GROUP_1:def 3
.= (Product ((yb1 | k9) ^ (yb1 /^ k9))) * (Product <*a*>) by GROUP_4:5
.= (Product yb1) * (Product <*a*>) by RFINSEQ:8
.= (eval (b1,x9)) * a by A22, GROUP_4:9 ;
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:14; :: thesis: verum

end;

end;