let n be Ordinal; for L being non trivial right_complementable Abelian add-associative right_zeroed well-unital distributive doubleLoopStr
for p, q being Polynomial of n,L
for x being Function of n,L
for b being bag of n st not b in Support p & Support q = (Support p) \/ {b} & ( for b9 being bag of n st b9 <> b holds
q . b9 = p . b9 ) holds
eval (q,x) = (eval (p,x)) + ((q . b) * (eval (b,x)))
let L be non trivial right_complementable Abelian add-associative right_zeroed well-unital distributive doubleLoopStr ; for p, q being Polynomial of n,L
for x being Function of n,L
for b being bag of n st not b in Support p & Support q = (Support p) \/ {b} & ( for b9 being bag of n st b9 <> b holds
q . b9 = p . b9 ) holds
eval (q,x) = (eval (p,x)) + ((q . b) * (eval (b,x)))
let p, q be Polynomial of n,L; for x being Function of n,L
for b being bag of n st not b in Support p & Support q = (Support p) \/ {b} & ( for b9 being bag of n st b9 <> b holds
q . b9 = p . b9 ) holds
eval (q,x) = (eval (p,x)) + ((q . b) * (eval (b,x)))
let x be Function of n,L; for b being bag of n st not b in Support p & Support q = (Support p) \/ {b} & ( for b9 being bag of n st b9 <> b holds
q . b9 = p . b9 ) holds
eval (q,x) = (eval (p,x)) + ((q . b) * (eval (b,x)))
let b be bag of n; ( not b in Support p & Support q = (Support p) \/ {b} & ( for b9 being bag of n st b9 <> b holds
q . b9 = p . b9 ) implies eval (q,x) = (eval (p,x)) + ((q . b) * (eval (b,x))) )
assume that
A1:
not b in Support p
and
A2:
Support q = (Support p) \/ {b}
and
A3:
for b9 being bag of n st b9 <> b holds
q . b9 = p . b9
; eval (q,x) = (eval (p,x)) + ((q . b) * (eval (b,x)))
set sq = SgmX ((BagOrder n),(Support q));
set sp = SgmX ((BagOrder n),(Support p));
A4:
BagOrder n linearly_orders Support q
by Th10;
b in {b}
by TARSKI:def 1;
then
b in Support q
by A2, XBOOLE_0:def 3;
then
b in rng (SgmX ((BagOrder n),(Support q)))
by A4, PRE_POLY:def 2;
then consider k being Nat such that
A5:
k in dom (SgmX ((BagOrder n),(Support q)))
and
A6:
(SgmX ((BagOrder n),(Support q))) . k = b
by FINSEQ_2:10;
A7:
(SgmX ((BagOrder n),(Support q))) /. k = b
by A5, A6, PARTFUN1:def 6;
reconsider b = b as Element of Bags n by PRE_POLY:def 12;
A8:
dom (SgmX ((BagOrder n),(Support q))) = Seg (len (SgmX ((BagOrder n),(Support q))))
by FINSEQ_1:def 3;
then A9:
k <= len (SgmX ((BagOrder n),(Support q)))
by A5, FINSEQ_1:1;
1 <= k
by A5, A8, 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;
A10:
k9 + 1 = k + 0
;
then A11:
SgmX ((BagOrder n),(Support q)) = Ins ((SgmX ((BagOrder n),(Support p))),k9,b)
by A1, A2, A5, A7, Th10, PRE_POLY:80;
consider yp being FinSequence of the carrier of L such that
A12:
len yp = len (SgmX ((BagOrder n),(Support p)))
and
A13:
Sum yp = eval (p,x)
and
A14:
for i being Element of NAT st 1 <= i & i <= len yp holds
yp /. i = ((p * (SgmX ((BagOrder n),(Support p)))) /. i) * (eval (((SgmX ((BagOrder n),(Support p))) /. i),x))
by Def2;
consider yq being FinSequence of the carrier of L such that
A15:
len yq = len (SgmX ((BagOrder n),(Support q)))
and
A16:
Sum yq = eval (q,x)
and
A17:
for i being Element of NAT st 1 <= i & i <= len yq holds
yq /. i = ((q * (SgmX ((BagOrder n),(Support q)))) /. i) * (eval (((SgmX ((BagOrder n),(Support q))) /. i),x))
by Def2;
VA:
dom yq = dom (SgmX ((BagOrder n),(Support q)))
by A15, FINSEQ_3:29;
reconsider b = b as Element of Bags n ;
set ytmp = Ins (yp,k9,((q . b) * (eval (b,x))));
A18: (len (SgmX ((BagOrder n),(Support p)))) + 1 =
(card (Support p)) + 1
by Th10, PRE_POLY:11
.=
card (Support q)
by A1, A2, CARD_2:41
.=
len (SgmX ((BagOrder n),(Support q)))
by Th10, PRE_POLY:11
;
then A19:
len yq = len (Ins (yp,k9,((q . b) * (eval (b,x)))))
by A15, A12, FINSEQ_5:69;
A20:
BagOrder n linearly_orders Support p
by Th10;
A21:
for i being Nat st 1 <= i & i <= len yq holds
yq . i = (Ins (yp,k9,((q . b) * (eval (b,x))))) . i
proof
let i be
Nat;
( 1 <= i & i <= len yq implies yq . i = (Ins (yp,k9,((q . b) * (eval (b,x))))) . i )
assume that A22:
1
<= i
and A23:
i <= len yq
;
yq . i = (Ins (yp,k9,((q . b) * (eval (b,x))))) . i
A24:
i in dom yq
by A22, A23, FINSEQ_3:25;
i in Seg (len (Ins (yp,k9,((q . b) * (eval (b,x))))))
by A19, A22, A23, FINSEQ_1:1;
then A25:
i in dom (Ins (yp,k9,((q . b) * (eval (b,x)))))
by FINSEQ_1:def 3;
per cases
( i = k or i <> k )
;
suppose A26:
i = k
;
yq . i = (Ins (yp,k9,((q . b) * (eval (b,x))))) . i
dom q = Bags n
by FUNCT_2:def 1;
then
(SgmX ((BagOrder n),(Support q))) . k in dom q
by A6, PRE_POLY:def 12;
then A27:
k in dom (q * (SgmX ((BagOrder n),(Support q))))
by A5, FUNCT_1:11;
then A28:
(q * (SgmX ((BagOrder n),(Support q)))) /. k =
(q * (SgmX ((BagOrder n),(Support q)))) . k
by PARTFUN1:def 6
.=
q . b
by A6, A27, FUNCT_1:12
;
A29:
yq /. i =
((q * (SgmX ((BagOrder n),(Support q)))) /. k) * (eval (((SgmX ((BagOrder n),(Support q))) /. k),x))
by A5, A17, A22, A23, A26
.=
(q . b) * (eval (b,x))
by A5, A6, A28, PARTFUN1:def 6
;
A30:
k9 <= len yp
by A9, A10, A12, A18, XREAL_1:6;
thus (Ins (yp,k9,((q . b) * (eval (b,x))))) . i =
(q . b) * (eval (b,x))
by A10, A26, A30, FINSEQ_5:73
.=
yq . i
by A24, A29, PARTFUN1:def 6
;
verum end; suppose A31:
i <> k
;
yq . i = (Ins (yp,k9,((q . b) * (eval (b,x))))) . i
len (Ins ((SgmX ((BagOrder n),(Support p))),k9,b)) = (len (SgmX ((BagOrder n),(Support p)))) + 1
by FINSEQ_5:69;
then A32:
dom (Ins ((SgmX ((BagOrder n),(Support p))),k9,b)) = Seg ((len (SgmX ((BagOrder n),(Support p)))) + 1)
by FINSEQ_1:def 3;
now ( ( i < k & yq . i = (Ins (yp,k9,((q . b) * (eval (b,x))))) . i ) or ( i > k & yq . i = (Ins (yp,k9,((q . b) * (eval (b,x))))) . i ) )per cases
( i < k or i > k )
by A31, XXREAL_0:1;
case A33:
i < k
;
yq . i = (Ins (yp,k9,((q . b) * (eval (b,x))))) . i
k9 < k
by A10, NAT_1:19;
then
k9 < len yq
by A9, A15, XXREAL_0:2;
then A34:
k9 <= len yp
by A15, A12, A18, NAT_1:13;
A35:
yp | (Seg k9) is
FinSequence
by FINSEQ_1:15;
A36:
i <= k9
by A10, A33, NAT_1:13;
then
i in Seg k9
by A22, FINSEQ_1:1;
then
i in dom (yp | (Seg k9))
by A34, A35, FINSEQ_1:17;
then A37:
i in dom (yp | k9)
by FINSEQ_1:def 16;
A38:
k - 1
<= ((len (SgmX ((BagOrder n),(Support p)))) + 1) - 1
by A9, A18, XREAL_1:9;
then A39:
i <= len (SgmX ((BagOrder n),(Support p)))
by A36, XXREAL_0:2;
then A40:
i in dom (SgmX ((BagOrder n),(Support p)))
by A22, FINSEQ_3:25;
i < len yq
by A9, A15, A33, XXREAL_0:2;
then A42:
i <= len yp
by A15, A12, A18, NAT_1:13;
then VV:
i in dom yp
by FINSEQ_3:25, A22;
A43:
(SgmX ((BagOrder n),(Support p))) | (Seg k9) is
FinSequence
by FINSEQ_1:15;
A44:
rng (Ins ((SgmX ((BagOrder n),(Support p))),k9,b)) c= Bags n
by FINSEQ_1:def 4;
A45:
dom q = Bags n
by FUNCT_2:def 1;
A46:
rng (SgmX ((BagOrder n),(Support p))) c= Bags n
by FINSEQ_1:def 4;
i in Seg k9
by A22, A36, FINSEQ_1:1;
then
i in dom ((SgmX ((BagOrder n),(Support p))) | (Seg k9))
by A38, A43, FINSEQ_1:17;
then A47:
i in dom ((SgmX ((BagOrder n),(Support p))) | k9)
by FINSEQ_1:def 16;
(SgmX ((BagOrder n),(Support p))) . i in rng (SgmX ((BagOrder n),(Support p)))
by A40, FUNCT_1:def 3;
then
(SgmX ((BagOrder n),(Support p))) . i in Bags n
by A46;
then
(SgmX ((BagOrder n),(Support p))) . i in dom p
by FUNCT_2:def 1;
then A48:
i in dom (p * (SgmX ((BagOrder n),(Support p))))
by A40, FUNCT_1:11;
len (SgmX ((BagOrder n),(Support p))) <= (len (SgmX ((BagOrder n),(Support p)))) + 1
by XREAL_1:29;
then
i <= (len (SgmX ((BagOrder n),(Support p)))) + 1
by A39, XXREAL_0:2;
then A49:
i in dom (Ins ((SgmX ((BagOrder n),(Support p))),k9,b))
by A22, A32, FINSEQ_1:1;
then
(Ins ((SgmX ((BagOrder n),(Support p))),k9,b)) . i in rng (Ins ((SgmX ((BagOrder n),(Support p))),k9,b))
by FUNCT_1:def 3;
then A50:
i in dom (q * (Ins ((SgmX ((BagOrder n),(Support p))),k9,b)))
by A49, A44, A45, FUNCT_1:11;
then A51:
(q * (Ins ((SgmX ((BagOrder n),(Support p))),k9,b))) . i =
q . ((Ins ((SgmX ((BagOrder n),(Support p))),k9,b)) . i)
by FUNCT_1:12
.=
q . ((SgmX ((BagOrder n),(Support p))) . i)
by A47, FINSEQ_5:72
.=
q . ((SgmX ((BagOrder n),(Support p))) /. i)
by A40, PARTFUN1:def 6
.=
p . ((SgmX ((BagOrder n),(Support p))) /. i)
by A3, A41
.=
p . ((SgmX ((BagOrder n),(Support p))) . i)
by A40, PARTFUN1:def 6
.=
(p * (SgmX ((BagOrder n),(Support p)))) . i
by A48, FUNCT_1:12
;
i in dom (q * (SgmX ((BagOrder n),(Support q))))
by A50, A11;
then Z:
(
(q * (SgmX ((BagOrder n),(Support q)))) /. i = (q * (SgmX ((BagOrder n),(Support q)))) . i &
(p * (SgmX ((BagOrder n),(Support p)))) /. i = (p * (SgmX ((BagOrder n),(Support p)))) . i )
by A48, PARTFUN1:def 6;
i in dom (SgmX ((BagOrder n),(Support q)))
by A24, VA;
then Z1:
(
(SgmX ((BagOrder n),(Support q))) /. i = (SgmX ((BagOrder n),(Support q))) . i &
(SgmX ((BagOrder n),(Support p))) /. i = (SgmX ((BagOrder n),(Support p))) . i )
by A40, PARTFUN1:def 6;
A52:
yq /. i =
((q * (SgmX ((BagOrder n),(Support q)))) /. i) * (eval (((SgmX ((BagOrder n),(Support q))) /. i),x))
by A17, A22, A23, A49
.=
((p * (SgmX ((BagOrder n),(Support p)))) /. i) * (eval (((SgmX ((BagOrder n),(Support p))) /. i),x))
by A11, A47, A51, FINSEQ_5:72, Z, Z1
.=
yp /. i
by A14, A22, A49, A42
.=
yp . i
by PARTFUN1:def 6, VV
.=
(Ins (yp,k9,((q . b) * (eval (b,x))))) . i
by A37, FINSEQ_5:72
.=
(Ins (yp,k9,((q . b) * (eval (b,x))))) /. i
by A25, PARTFUN1:def 6
;
thus yq . i =
yq /. i
by A24, PARTFUN1:def 6
.=
(Ins (yp,k9,((q . b) * (eval (b,x))))) . i
by A25, A52, PARTFUN1:def 6
;
verum end; case A53:
i > k
;
yq . i = (Ins (yp,k9,((q . b) * (eval (b,x))))) . ithen
i - 1
> k9
by XREAL_1:9;
then reconsider i1 =
i - 1 as
Element of
NAT by INT_1:3;
A54:
(i - 1) + 1
= i + 0
;
then A55:
k9 + 1
<= i1
by A53, NAT_1:13;
A56:
dom q = Bags n
by FUNCT_2:def 1;
A57:
rng (Ins ((SgmX ((BagOrder n),(Support p))),k9,b)) c= Bags n
by FINSEQ_1:def 4;
A58:
dom p = Bags n
by FUNCT_2:def 1;
A59:
rng (SgmX ((BagOrder n),(Support p))) c= Bags n
by FINSEQ_1:def 4;
A60:
i - 1
<= ((len yp) + 1) - 1
by A15, A12, A18, A23, XREAL_1:9;
0 + 1
<= k9 + 1
by XREAL_1:6;
then
1
< i
by A53, XXREAL_0:2;
then A61:
1
<= i1
by A54, NAT_1:13;
then
i1 in Seg (len (SgmX ((BagOrder n),(Support p))))
by A12, A60, FINSEQ_1:1;
then A62:
i1 in dom (SgmX ((BagOrder n),(Support p)))
by FINSEQ_1:def 3;
dom yp = dom (SgmX ((BagOrder n),(Support p)))
by A12, FINSEQ_3:29;
then AA:
i1 in dom yp
by A62;
(SgmX ((BagOrder n),(Support p))) . i1 in rng (SgmX ((BagOrder n),(Support p)))
by A62, FUNCT_1:def 3;
then A64:
i1 in dom (p * (SgmX ((BagOrder n),(Support p))))
by A62, A59, A58, FUNCT_1:11;
A65:
i = i1 + 1
;
A66:
i in dom (Ins ((SgmX ((BagOrder n),(Support p))),k9,b))
by A15, A18, A22, A23, A32, FINSEQ_1:1;
then
(Ins ((SgmX ((BagOrder n),(Support p))),k9,b)) . i in rng (Ins ((SgmX ((BagOrder n),(Support p))),k9,b))
by FUNCT_1:def 3;
then A67:
i in dom (q * (Ins ((SgmX ((BagOrder n),(Support p))),k9,b)))
by A66, A57, A56, FUNCT_1:11;
then A68:
(q * (Ins ((SgmX ((BagOrder n),(Support p))),k9,b))) . i =
q . ((Ins ((SgmX ((BagOrder n),(Support p))),k9,b)) . i)
by FUNCT_1:12
.=
q . ((SgmX ((BagOrder n),(Support p))) . i1)
by A12, A60, A65, A55, FINSEQ_5:74
.=
q . ((SgmX ((BagOrder n),(Support p))) /. i1)
by A62, PARTFUN1:def 6
.=
p . ((SgmX ((BagOrder n),(Support p))) /. i1)
by A3, A63
.=
p . ((SgmX ((BagOrder n),(Support p))) . i1)
by A62, PARTFUN1:def 6
.=
(p * (SgmX ((BagOrder n),(Support p)))) . i1
by A64, FUNCT_1:12
;
BB:
dom yq = dom (SgmX ((BagOrder n),(Support q)))
by FINSEQ_3:29, A15;
SS:
(q * (SgmX ((BagOrder n),(Support q)))) /. i =
(q * (SgmX ((BagOrder n),(Support q)))) . i
by A67, PARTFUN1:def 6, A11
.=
(p * (SgmX ((BagOrder n),(Support p)))) /. i1
by A64, PARTFUN1:def 6, A68, A11
;
SA:
(SgmX ((BagOrder n),(Support q))) /. i =
(SgmX ((BagOrder n),(Support q))) . i
by A24, BB, PARTFUN1:def 6
.=
(SgmX ((BagOrder n),(Support p))) . i1
by A12, A60, A65, A55, A11, FINSEQ_5:74
.=
(SgmX ((BagOrder n),(Support p))) /. i1
by PARTFUN1:def 6, A62
;
A69:
yq /. i =
((q * (SgmX ((BagOrder n),(Support q)))) /. i) * (eval (((SgmX ((BagOrder n),(Support q))) /. i),x))
by A17, A22, A23, A66
.=
yp /. i1
by A14, A60, A61, SS, SA
.=
yp . i1
by PARTFUN1:def 6, AA
.=
(Ins (yp,k9,((q . b) * (eval (b,x))))) . i
by A60, A65, A55, FINSEQ_5:74
.=
(Ins (yp,k9,((q . b) * (eval (b,x))))) /. i
by PARTFUN1:def 6, A25
;
thus yq . i =
yq /. i
by A24, PARTFUN1:def 6
.=
(Ins (yp,k9,((q . b) * (eval (b,x))))) . i
by A25, A69, PARTFUN1:def 6
;
verum end; hence
yq . i = (Ins (yp,k9,((q . b) * (eval (b,x))))) . i
;
verum end;
end;
Sum (((yp | k9) ^ <*((q . b) * (eval (b,x)))*>) ^ (yp /^ k9)) =
(Sum ((yp | k9) ^ <*((q . b) * (eval (b,x)))*>)) + (Sum (yp /^ k9))
by RLVECT_1:41
.=
((Sum (yp | k9)) + (Sum <*((q . b) * (eval (b,x)))*>)) + (Sum (yp /^ k9))
by RLVECT_1:41
.=
((Sum (yp | k9)) + (Sum (yp /^ k9))) + (Sum <*((q . b) * (eval (b,x)))*>)
by RLVECT_1:def 3
.=
(Sum ((yp | k9) ^ (yp /^ k9))) + (Sum <*((q . b) * (eval (b,x)))*>)
by RLVECT_1:41
.=
(Sum yp) + (Sum <*((q . b) * (eval (b,x)))*>)
by RFINSEQ:8
.=
(eval (p,x)) + ((q . b) * (eval (b,x)))
by A13, RLVECT_1:44
;
then
Sum (Ins (yp,k9,((q . b) * (eval (b,x))))) = (eval (p,x)) + ((q . b) * (eval (b,x)))
by FINSEQ_5:def 4;
hence
eval (q,x) = (eval (p,x)) + ((q . b) * (eval (b,x)))
by A16, A19, A21, FINSEQ_1:14; verum