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
for u being set st not u in support b1 & support b2 = (support b1) \/ {u} & ( for u' being set st u' <> u holds
b2 . u' = b1 . u' ) 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
for u being set st not u in support b1 & support b2 = (support b1) \/ {u} & ( for u' being set st u' <> u holds
b2 . u' = b1 . u' ) 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 ; :: thesis: for u being set st not u in support b1 & support b2 = (support b1) \/ {u} & ( for u' being set st u' <> u holds
b2 . u' = b1 . u' ) 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 u' being set st u' <> u holds
b2 . u' = b1 . u' ) 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 A1: ( not u in support b1 & support b2 = (support b1) \/ {u} & ( for u' being set st u' <> u holds
b2 . u' = b1 . u' ) ) ; :: 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)
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)
A2: 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 A3: a = (power L) . (x . u),(b2 . u) ; :: thesis: eval b2,x = a * (eval b1,x)
set sb2 = SgmX (RelIncl n),(support b2);
set sb1 = SgmX (RelIncl n),(support b1);
A4: ( RelIncl n linearly_orders support b2 & RelIncl n linearly_orders support b1 ) by Th15;
u in {u} by TARSKI:def 1;
then A5: u in support b2 by A1, XBOOLE_0:def 3;
then u in rng (SgmX (RelIncl n),(support b2)) by A4, TRIANG_1:def 2;
then consider k being Nat such that
A6: ( k in dom (SgmX (RelIncl n),(support b2)) & (SgmX (RelIncl n),(support b2)) . k = u ) by FINSEQ_2:11;
A7: (SgmX (RelIncl n),(support b2)) /. k = u by A6, PARTFUN1:def 8;
dom (SgmX (RelIncl n),(support b2)) = Seg (len (SgmX (RelIncl n),(support b2))) by FINSEQ_1:def 3;
then A8: ( 1 <= k & k <= len (SgmX (RelIncl n),(support b2)) ) by A6, FINSEQ_1:3;
then 1 - 1 <= k - 1 by XREAL_1:11;
then reconsider k' = k - 1 as Element of NAT by INT_1:16;
reconsider u = u as Element of n by A5;
A9: k' + 1 = k + 0 ;

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

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

then A10: Bags n = {(EmptyBag n)} by POLYNOM1:55, TARSKI:def 1;
( b1 in Bags n & b2 in Bags n ) by POLYNOM1:def 14;
then A11: ( b1 = EmptyBag n & b2 = EmptyBag n ) by A10, TARSKI:def 1;
u in {u} by TARSKI:def 1;
then u in support b2 by A1, XBOOLE_0:def 3;
then b2 . u <> 0 by POLYNOM1:def 7;
hence eval b2,x = a * (eval b1,x) by A11, POLYNOM1:56; :: thesis: verum

end;

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

then reconsider n' = n as non empty Ordinal ;
reconsider x' = x as Function of n',L ;
reconsider b1 = b1, b2 = b2 as bag of ;
reconsider sb2 = SgmX (RelIncl n),(support b2), sb1 = SgmX (RelIncl n),(support b1) as FinSequence of n' ;
reconsider u = u as Element of n' ;
A12: sb2 = Ins sb1,k',u by A1, A4, A6, A7, A9, Th13;
consider yb2 being FinSequence of the carrier of L such that
A13: ( len yb2 = len sb2 & eval b2,x' = Product yb2 & ( 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
A14: ( len yb1 = len sb1 & eval b1,x' = Product yb1 & ( 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,k',a;
Product (((yb1 | k') ^ <*a*>) ^ (yb1 /^ k')) = (Product ((yb1 | k') ^ <*a*>)) * (Product (yb1 /^ k')) by GROUP_4:8
.= ((Product (yb1 | k')) * (Product <*a*>)) * (Product (yb1 /^ k')) by GROUP_4:8
.= ((Product (yb1 | k')) * (Product (yb1 /^ k'))) * (Product <*a*>) by GROUP_1:def 4
.= (Product ((yb1 | k') ^ (yb1 /^ k'))) * (Product <*a*>) by GROUP_4:8
.= (Product yb1) * (Product <*a*>) by RFINSEQ:21
.= (eval b1,x') * a by A14, GROUP_4:12 ;
then A15: Product (Ins yb1,k',a) = (eval b1,x') * a by FINSEQ_5:def 4;
A16: (len sb1) + 1 = (card (support b1)) + 1 by Th15, TRIANG_1:9
.= card (support b2) by A1, CARD_2:54
.= len sb2 by Th15, TRIANG_1:9 ;
then A17: len yb2 = len (Ins yb1,k',a) by A13, A14, FINSEQ_5:72;
for i being Nat st 1 <= i & i <= len yb2 holds
yb2 . i = (Ins yb1,k',a) . i

proof

let i be Nat; :: thesis: ( 1 <= i & i <= len yb2 implies yb2 . i = (Ins yb1,k',a) . i )
assume A18: ( 1 <= i & i <= len yb2 ) ; :: thesis: yb2 . i = (Ins yb1,k',a) . i
then A19: ( i in Seg (len yb2) & i in Seg (len (Ins yb1,k',a)) ) by A17, FINSEQ_1:3;
then A20: ( i in dom yb2 & i in dom (Ins yb1,k',a) ) by FINSEQ_1:def 3;
A21: yb2 /. i = (power L) . ((x * (Ins sb1,k',u)) /. i),((b2 * (Ins sb1,k',u)) /. i) by A12, A13, A18, A19;
A22: 1 - 1 <= i - 1 by A18, XREAL_1:11;
then A23: i - 1 is Element of NAT by INT_1:16;

now

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

case A24: i = k ; :: thesis: (Ins yb1,k',a) . i = yb2 . i

then A25: k' <= len yb1 by A9, A13, A14, A16, A18, XREAL_1:8;
A26: sb2 . k in {u} by A6, TARSKI:def 1;
then A27: sb2 . k in support b2 by A1, XBOOLE_0:def 3;
support b2 c= dom b2 by POLYNOM1:41;
then A28: k in dom (b2 * sb2) by A6, A27, FUNCT_1:21;
then A29: (b2 * sb2) /. k = (b2 * sb2) . k by PARTFUN1:def 8
.= b2 . u by A6, A28, FUNCT_1:22 ;
A30: k in dom (x * sb2) by A2, A6, A26, FUNCT_1:21;
then (x * sb2) /. k = (x * sb2) . k by PARTFUN1:def 8
.= x . u by A6, A30, FUNCT_1:22 ;
then A31: yb2 /. i = (power L) . (x . u),(b2 . u) by A13, A18, A19, A24, A29;
thus (Ins yb1,k',a) . i = (Ins yb1,k',a) /. i by A20, PARTFUN1:def 8
.= yb2 /. i by A3, A9, A24, A25, A31, FINSEQ_5:76
.= yb2 . i by A20, PARTFUN1:def 8 ; :: thesis: verum

end;

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

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

now

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

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

then A35: i <= k' by A9, NAT_1:13;
then A36: i in Seg k' by A18, FINSEQ_1:3;
A37: k - 1 <= ((len sb1) + 1) - 1 by A8, A16, XREAL_1:11;
A38: i < len yb2 by A8, A13, A34, XXREAL_0:2;
then A39: i <= len sb1 by A13, A16, NAT_1:13;
sb1 | (Seg k') is FinSequence by FINSEQ_1:19;
then i in dom (sb1 | (Seg k')) by A36, A37, FINSEQ_1:21;
then A40: i in dom (sb1 | k') by FINSEQ_1:def 15;
i <= (len sb1) + 1 by A8, A16, A34, XXREAL_0:2;
then A41: i in dom (Ins sb1,k',u) by A18, A33, FINSEQ_1:3;
then A42: (Ins sb1,k',u) . i in rng (Ins sb1,k',u) by FUNCT_1:def 5;
A43: rng (Ins sb1,k',u) c= n by FINSEQ_1:def 4;
i in Seg (len sb1) by A18, A39, FINSEQ_1:3;
then A44: i in dom sb1 by FINSEQ_1:def 3;
then A45: sb1 . i in rng sb1 by FUNCT_1:def 5;
A46: rng sb1 c= n by FINSEQ_1:def 4;
then sb1 . i in n by A45;
then sb1 . i in dom b1 by PARTFUN1:def 4;
then A47: i in dom (b1 * sb1) by A44, FUNCT_1:21;

A48: now

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

end;

A49: i <= len yb1 by A13, A14, A16, A38, NAT_1:13;
A50: i in Seg k' by A18, A35, FINSEQ_1:3;
A51: k' <= len yb1 by A8, A9, A14, A16, XREAL_1:8;
yb1 | (Seg k') is FinSequence by FINSEQ_1:19;
then i in dom (yb1 | (Seg k')) by A50, A51, FINSEQ_1:21;
then A52: i in dom (yb1 | k') by FINSEQ_1:def 15;
dom b2 = n by PARTFUN1:def 4;
then A53: i in dom (b2 * (Ins sb1,k',u)) by A41, A42, A43, FUNCT_1:21;
A54: i in dom (x * sb1) by A2, A44, A45, A46, FUNCT_1:21;
A55: i in dom (x * (Ins sb1,k',u)) by A2, A41, A42, A43, FUNCT_1:21;
then A56: (x * (Ins sb1,k',u)) /. i = (x * (Ins sb1,k',u)) . i by PARTFUN1:def 8
.= x . ((Ins sb1,k',u) . i) by A55, FUNCT_1:22
.= x . ((Ins sb1,k',u) /. i) by A41, PARTFUN1:def 8
.= x . (sb1 /. i) by A40, FINSEQ_5:75
.= x . (sb1 . i) by A44, PARTFUN1:def 8
.= (x * sb1) . i by A54, FUNCT_1:22
.= (x * sb1) /. i by A54, PARTFUN1:def 8 ;
(b2 * (Ins sb1,k',u)) /. i = (b2 * (Ins sb1,k',u)) . i by A53, PARTFUN1:def 8
.= b2 . ((Ins sb1,k',u) . i) by A53, FUNCT_1:22
.= b2 . ((Ins sb1,k',u) /. i) by A41, PARTFUN1:def 8
.= b2 . (sb1 /. i) by A40, FINSEQ_5:75
.= b1 . (sb1 /. i) by A1, A48
.= b1 . (sb1 . i) by A44, PARTFUN1:def 8
.= (b1 * sb1) . i by A47, FUNCT_1:22
.= (b1 * sb1) /. i by A47, PARTFUN1:def 8 ;
then A57: yb2 /. i = yb1 /. i by A14, A18, A19, A21, A49, A56
.= (Ins yb1,k',a) /. i by A52, FINSEQ_5:75 ;
thus yb2 . i = yb2 /. i by A20, PARTFUN1:def 8
.= (Ins yb1,k',a) . i by A20, A57, PARTFUN1:def 8 ; :: thesis: verum

end;

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

A59: (i - 1) + 1 = i + 0 ;
1 < i by A8, A58, XXREAL_0:2;
then A60: 1 <= i - 1 by A23, A59, NAT_1:13;
reconsider i1 = i - 1 as Element of NAT by A22, INT_1:16;
A61: i - 1 <= (len sb2) - 1 by A13, A18, XREAL_1:11;
A62: i1 + 1 = i + 0 ;
i1 in Seg (len sb1) by A16, A60, A61, FINSEQ_1:3;
then A63: i1 in dom sb1 by FINSEQ_1:def 3;

A64: now

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

end;

A65: sb1 . i1 in rng sb1 by A63, FUNCT_1:def 5;
A66: rng sb1 c= n by FINSEQ_1:def 4;
dom b1 = n by PARTFUN1:def 4;
then A67: i1 in dom (b1 * sb1) by A63, A65, A66, FUNCT_1:21;
A68: i in dom (Ins sb1,k',u) by A13, A16, A18, A33, FINSEQ_1:3;
then A69: (Ins sb1,k',u) . i in rng (Ins sb1,k',u) by FUNCT_1:def 5;
A70: rng (Ins sb1,k',u) c= n by FINSEQ_1:def 4;
A71: i = i1 + 1 ;
A72: i1 in dom (x * sb1) by A2, A63, A65, A66, FUNCT_1:21;
A73: k' + 1 <= i1 by A58, A62, NAT_1:13;
A74: i in dom (x * (Ins sb1,k',u)) by A2, A68, A69, A70, FUNCT_1:21;
then A75: (x * (Ins sb1,k',u)) /. i = (x * (Ins sb1,k',u)) . i by PARTFUN1:def 8
.= x . ((Ins sb1,k',u) . i) by A74, FUNCT_1:22
.= x . ((Ins sb1,k',u) /. i) by A68, PARTFUN1:def 8
.= x . (sb1 /. i1) by A16, A61, A62, A73, FINSEQ_5:77
.= x . (sb1 . i1) by A63, PARTFUN1:def 8
.= (x * sb1) . i1 by A72, FUNCT_1:22
.= (x * sb1) /. i1 by A72, PARTFUN1:def 8 ;
dom b2 = n by PARTFUN1:def 4;
then A76: i in dom (b2 * (Ins sb1,k',u)) by A68, A69, A70, FUNCT_1:21;
then (b2 * (Ins sb1,k',u)) /. i = (b2 * (Ins sb1,k',u)) . i by PARTFUN1:def 8
.= b2 . ((Ins sb1,k',u) . i) by A76, FUNCT_1:22
.= b2 . ((Ins sb1,k',u) /. i) by A68, PARTFUN1:def 8
.= b2 . (sb1 /. i1) by A16, A61, A62, A73, FINSEQ_5:77
.= b1 . (sb1 /. i1) by A1, A64
.= b1 . (sb1 . i1) by A63, PARTFUN1:def 8
.= (b1 * sb1) . i1 by A67, FUNCT_1:22
.= (b1 * sb1) /. i1 by A67, PARTFUN1:def 8 ;
then A77: yb2 /. i = yb1 /. i1 by A14, A16, A21, A60, A61, A75
.= (Ins yb1,k',a) /. i by A14, A16, A61, A71, A73, FINSEQ_5:77 ;
thus yb2 . i = yb2 /. i by A20, PARTFUN1:def 8
.= (Ins yb1,k',a) . i by A20, A77, PARTFUN1:def 8 ; :: thesis: verum

end;

end;

end;

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

end;

end;

end;

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

end;

hence eval b2,x = a * (eval b1,x) by A13, A15, A17, FINSEQ_1:18; :: thesis: verum

end;

end;