let n be Ordinal; 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 ; 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; 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 ; ( 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
; 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; 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; ( a = (power L) . ((x . u),(b2 . u)) implies eval (b2,x) = a * (eval (b1,x)) )
assume A6:
a = (power L) . ((x . u),(b2 . u))
; 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
n <> {}
;
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;
( 1 <= i & i <= len yb2 implies yb2 . i = (Ins (yb1,k9,a)) . i )
assume that A28:
1
<= i
and A29:
i <= len yb2
;
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 ( ( 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
;
(Ins (yb1,k9,a)) . i = yb2 . iA37:
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;
verum end; case A44:
i <> k
;
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 ( ( 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
;
yb2 . i = (Ins (yb1,k9,a)) . ithen 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 15;
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 not sb1 . i = uend; 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 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: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
;
verum end; case A69:
i > k
;
yb2 . i = (Ins (yb1,k9,a)) . ireconsider 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 not sb1 /. i1 = uend; 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
;
verum end; hence
yb2 . i = (Ins (yb1,k9,a)) . i
;
verum end;
hence
yb2 . i = (Ins (yb1,k9,a)) . i
;
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;
verum end;