let n be Ordinal; for b being bag of n
for f, g being FinSequence of (3 -tuples_on (Bags n)) * st dom f = dom (decomp b) & dom g = dom (decomp b) & ( for k being Nat st k in dom f holds
f . k = (decomp (((decomp b) /. k) /. 1)) ^^ ((len (decomp (((decomp b) /. k) /. 1))) |-> <*(((decomp b) /. k) /. 2)*>) ) & ( for k being Nat st k in dom g holds
g . k = ((len (decomp (((decomp b) /. k) /. 2))) |-> <*(((decomp b) /. k) /. 1)*>) ^^ (decomp (((decomp b) /. k) /. 2)) ) holds
ex p being Permutation of (dom (FlattenSeq f)) st FlattenSeq g = (FlattenSeq f) * p
let b be bag of n; for f, g being FinSequence of (3 -tuples_on (Bags n)) * st dom f = dom (decomp b) & dom g = dom (decomp b) & ( for k being Nat st k in dom f holds
f . k = (decomp (((decomp b) /. k) /. 1)) ^^ ((len (decomp (((decomp b) /. k) /. 1))) |-> <*(((decomp b) /. k) /. 2)*>) ) & ( for k being Nat st k in dom g holds
g . k = ((len (decomp (((decomp b) /. k) /. 2))) |-> <*(((decomp b) /. k) /. 1)*>) ^^ (decomp (((decomp b) /. k) /. 2)) ) holds
ex p being Permutation of (dom (FlattenSeq f)) st FlattenSeq g = (FlattenSeq f) * p
let f, g be FinSequence of (3 -tuples_on (Bags n)) * ; ( dom f = dom (decomp b) & dom g = dom (decomp b) & ( for k being Nat st k in dom f holds
f . k = (decomp (((decomp b) /. k) /. 1)) ^^ ((len (decomp (((decomp b) /. k) /. 1))) |-> <*(((decomp b) /. k) /. 2)*>) ) & ( for k being Nat st k in dom g holds
g . k = ((len (decomp (((decomp b) /. k) /. 2))) |-> <*(((decomp b) /. k) /. 1)*>) ^^ (decomp (((decomp b) /. k) /. 2)) ) implies ex p being Permutation of (dom (FlattenSeq f)) st FlattenSeq g = (FlattenSeq f) * p )
assume that
A1:
dom f = dom (decomp b)
and
A2:
dom g = dom (decomp b)
and
A3:
for k being Nat st k in dom f holds
f . k = (decomp (((decomp b) /. k) /. 1)) ^^ ((len (decomp (((decomp b) /. k) /. 1))) |-> <*(((decomp b) /. k) /. 2)*>)
and
A4:
for k being Nat st k in dom g holds
g . k = ((len (decomp (((decomp b) /. k) /. 2))) |-> <*(((decomp b) /. k) /. 1)*>) ^^ (decomp (((decomp b) /. k) /. 2))
; ex p being Permutation of (dom (FlattenSeq f)) st FlattenSeq g = (FlattenSeq f) * p
set Ff = FlattenSeq f;
set Fg = FlattenSeq g;
set db = decomp b;
A5:
FlattenSeq g is one-to-one
proof
let k1,
k2 be
set ;
FUNCT_1:def 8 ( not k1 in proj1 (FlattenSeq g) or not k2 in proj1 (FlattenSeq g) or not (FlattenSeq g) . k1 = (FlattenSeq g) . k2 or k1 = k2 )
assume that A6:
k1 in dom (FlattenSeq g)
and A7:
k2 in dom (FlattenSeq g)
and A8:
(FlattenSeq g) . k1 = (FlattenSeq g) . k2
;
k1 = k2
consider i1,
j1 being
Element of
NAT such that A9:
i1 in dom g
and A10:
j1 in dom (g . i1)
and A11:
k1 = (Sum (Card (g | (i1 -' 1)))) + j1
and A12:
(g . i1) . j1 = (FlattenSeq g) . k1
by A6, Th32;
set ddbi11 =
decomp (((decomp b) /. i1) /. 2);
A13:
g . i1 = ((len (decomp (((decomp b) /. i1) /. 2))) |-> <*(((decomp b) /. i1) /. 1)*>) ^^ (decomp (((decomp b) /. i1) /. 2))
by A4, A9;
then A14:
dom (g . i1) =
(dom (decomp (((decomp b) /. i1) /. 2))) /\ (dom ((len (decomp (((decomp b) /. i1) /. 2))) |-> <*(((decomp b) /. i1) /. 1)*>))
by Def2M
.=
(dom (decomp (((decomp b) /. i1) /. 2))) /\ (Seg (len (decomp (((decomp b) /. i1) /. 2))))
by FUNCOP_1:19
.=
(dom (decomp (((decomp b) /. i1) /. 2))) /\ (dom (decomp (((decomp b) /. i1) /. 2)))
by FINSEQ_1:def 3
.=
dom (decomp (((decomp b) /. i1) /. 2))
;
then A15:
(decomp (((decomp b) /. i1) /. 2)) /. j1 = (decomp (((decomp b) /. i1) /. 2)) . j1
by A10, PARTFUN1:def 8;
dom (decomp (((decomp b) /. i1) /. 2)) = Seg (len (decomp (((decomp b) /. i1) /. 2)))
by FINSEQ_1:def 3;
then A16:
((len (decomp (((decomp b) /. i1) /. 2))) |-> <*(((decomp b) /. i1) /. 1)*>) . j1 = <*(((decomp b) /. i1) /. 1)*>
by A10, A14, FUNCOP_1:13;
consider b11,
b12 being
bag of
n such that A17:
(decomp b) /. i1 = <*b11,b12*>
and
b = b11 + b12
by A2, A9, Th72;
reconsider b119 =
b11,
b129 =
b12 as
Element of
Bags n by Def14;
A18:
(
b119 = b11 &
b129 = b12 )
;
then
((decomp b) /. i1) /. 2
= b12
by A17, FINSEQ_4:26;
then consider b111,
b112 being
bag of
n such that A19:
(decomp (((decomp b) /. i1) /. 2)) /. j1 = <*b111,b112*>
and A20:
b12 = b111 + b112
by A10, A14, Th72;
((decomp b) /. i1) /. 1
= b11
by A17, A18, FINSEQ_4:26;
then A21:
(g . i1) . j1 =
<*b11*> ^ <*b111,b112*>
by A10, A13, A19, A15, A16, Def2M
.=
<*b11,b111,b112*>
by FINSEQ_1:60
;
consider i2,
j2 being
Element of
NAT such that A22:
i2 in dom g
and A23:
j2 in dom (g . i2)
and A24:
k2 = (Sum (Card (g | (i2 -' 1)))) + j2
and A25:
(g . i2) . j2 = (FlattenSeq g) . k2
by A7, Th32;
set ddbi21 =
decomp (((decomp b) /. i2) /. 2);
A26:
g . i2 = ((len (decomp (((decomp b) /. i2) /. 2))) |-> <*(((decomp b) /. i2) /. 1)*>) ^^ (decomp (((decomp b) /. i2) /. 2))
by A4, A22;
then A27:
dom (g . i2) =
(dom (decomp (((decomp b) /. i2) /. 2))) /\ (dom ((len (decomp (((decomp b) /. i2) /. 2))) |-> <*(((decomp b) /. i2) /. 1)*>))
by Def2M
.=
(dom (decomp (((decomp b) /. i2) /. 2))) /\ (Seg (len (decomp (((decomp b) /. i2) /. 2))))
by FUNCOP_1:19
.=
(dom (decomp (((decomp b) /. i2) /. 2))) /\ (dom (decomp (((decomp b) /. i2) /. 2)))
by FINSEQ_1:def 3
.=
dom (decomp (((decomp b) /. i2) /. 2))
;
then A28:
(decomp (((decomp b) /. i2) /. 2)) /. j2 = (decomp (((decomp b) /. i2) /. 2)) . j2
by A23, PARTFUN1:def 8;
dom (decomp (((decomp b) /. i2) /. 2)) = Seg (len (decomp (((decomp b) /. i2) /. 2)))
by FINSEQ_1:def 3;
then A29:
((len (decomp (((decomp b) /. i2) /. 2))) |-> <*(((decomp b) /. i2) /. 1)*>) . j2 = <*(((decomp b) /. i2) /. 1)*>
by A23, A27, FUNCOP_1:13;
consider b21,
b22 being
bag of
n such that A30:
(decomp b) /. i2 = <*b21,b22*>
and
b = b21 + b22
by A2, A22, Th72;
reconsider b219 =
b21,
b229 =
b22 as
Element of
Bags n by Def14;
A31:
(
b219 = b21 &
b229 = b22 )
;
then
((decomp b) /. i2) /. 2
= b22
by A30, FINSEQ_4:26;
then consider b211,
b212 being
bag of
n such that A32:
(decomp (((decomp b) /. i2) /. 2)) /. j2 = <*b211,b212*>
and A33:
b22 = b211 + b212
by A23, A27, Th72;
((decomp b) /. i2) /. 1
= b21
by A30, A31, FINSEQ_4:26;
then A34:
(g . i2) . j2 =
<*b21*> ^ <*b211,b212*>
by A23, A26, A32, A28, A29, Def2M
.=
<*b21,b211,b212*>
by FINSEQ_1:60
;
then A35:
(
b111 = b211 &
b112 = b212 )
by A8, A12, A25, A21, FINSEQ_1:99;
A36:
(decomp b) /. i2 = (decomp b) . i2
by A2, A22, PARTFUN1:def 8;
A37:
(decomp b) /. i1 = (decomp b) . i1
by A2, A9, PARTFUN1:def 8;
b11 = b21
by A8, A12, A25, A21, A34, FINSEQ_1:99;
then
i1 = i2
by A2, A9, A22, A37, A17, A20, A36, A30, A33, A35, FUNCT_1:def 8;
hence
k1 = k2
by A10, A11, A23, A24, A19, A15, A27, A32, A28, A35, FUNCT_1:def 8;
verum
end;
now let y be
set ;
( ( y in rng (FlattenSeq f) implies y in rng (FlattenSeq g) ) & ( y in rng (FlattenSeq g) implies y in rng (FlattenSeq f) ) )hereby ( y in rng (FlattenSeq g) implies y in rng (FlattenSeq f) )
assume
y in rng (FlattenSeq f)
;
y in rng (FlattenSeq g)then consider k being
set such that A38:
k in dom (FlattenSeq f)
and A39:
y = (FlattenSeq f) . k
by FUNCT_1:def 5;
reconsider k =
k as
Element of
NAT by A38;
consider i,
j being
Element of
NAT such that A40:
i in dom f
and A41:
j in dom (f . i)
and
k = (Sum (Card (f | (i -' 1)))) + j
and A42:
(f . i) . j = (FlattenSeq f) . k
by A38, Th32;
set ddbi1 =
decomp (((decomp b) /. i) /. 1);
A43:
f . i = (decomp (((decomp b) /. i) /. 1)) ^^ ((len (decomp (((decomp b) /. i) /. 1))) |-> <*(((decomp b) /. i) /. 2)*>)
by A3, A40;
then A44:
dom (f . i) =
(dom (decomp (((decomp b) /. i) /. 1))) /\ (dom ((len (decomp (((decomp b) /. i) /. 1))) |-> <*(((decomp b) /. i) /. 2)*>))
by Def2M
.=
(dom (decomp (((decomp b) /. i) /. 1))) /\ (Seg (len (decomp (((decomp b) /. i) /. 1))))
by FUNCOP_1:19
.=
(dom (decomp (((decomp b) /. i) /. 1))) /\ (dom (decomp (((decomp b) /. i) /. 1)))
by FINSEQ_1:def 3
.=
dom (decomp (((decomp b) /. i) /. 1))
;
dom (decomp (((decomp b) /. i) /. 1)) = Seg (len (decomp (((decomp b) /. i) /. 1)))
by FINSEQ_1:def 3;
then A45:
((len (decomp (((decomp b) /. i) /. 1))) |-> <*(((decomp b) /. i) /. 2)*>) . j = <*(((decomp b) /. i) /. 2)*>
by A41, A44, FUNCOP_1:13;
consider b1,
b2 being
bag of
n such that A46:
(decomp b) /. i = <*b1,b2*>
and A47:
b = b1 + b2
by A1, A40, Th72;
reconsider b19 =
b1,
b29 =
b2 as
Element of
Bags n by Def14;
A48:
(
b19 = b1 &
b29 = b2 )
;
then A49:
((decomp b) /. i) /. 2
= b2
by A46, FINSEQ_4:26;
((decomp b) /. i) /. 1
= b1
by A46, A48, FINSEQ_4:26;
then consider b11,
b12 being
bag of
n such that A50:
(decomp (((decomp b) /. i) /. 1)) /. j = <*b11,b12*>
and A51:
b1 = b11 + b12
by A41, A44, Th72;
b = b11 + (b12 + b2)
by A47, A51, Th39;
then consider i9 being
Element of
NAT such that A52:
i9 in dom (decomp b)
and A53:
(decomp b) /. i9 = <*b11,(b12 + b2)*>
by Th73;
set b3 =
b12 + b2;
reconsider b119 =
b11,
b39 =
b12 + b2 as
Element of
Bags n by Def14;
consider j9 being
Element of
NAT such that A54:
j9 in dom (decomp (b12 + b2))
and A55:
(decomp (b12 + b2)) /. j9 = <*b12,b2*>
by Th73;
set ddbi92 =
decomp (((decomp b) /. i9) /. 2);
A56:
(decomp b) /. i9 = <*b119,b39*>
by A53;
then A57:
(
((decomp b) /. i9) /. 1
= b11 &
decomp (((decomp b) /. i9) /. 2) = decomp (b12 + b2) )
by FINSEQ_4:26;
A58:
g . i9 = ((len (decomp (((decomp b) /. i9) /. 2))) |-> <*(((decomp b) /. i9) /. 1)*>) ^^ (decomp (((decomp b) /. i9) /. 2))
by A2, A4, A52;
then A59:
dom (g . i9) =
(dom ((len (decomp (((decomp b) /. i9) /. 2))) |-> <*(((decomp b) /. i9) /. 1)*>)) /\ (dom (decomp (((decomp b) /. i9) /. 2)))
by Def2M
.=
(Seg (len (decomp (((decomp b) /. i9) /. 2)))) /\ (dom (decomp (((decomp b) /. i9) /. 2)))
by FUNCOP_1:19
.=
(dom (decomp (((decomp b) /. i9) /. 2))) /\ (dom (decomp (((decomp b) /. i9) /. 2)))
by FINSEQ_1:def 3
.=
dom (decomp (((decomp b) /. i9) /. 2))
;
then A60:
j9 in dom (g . i9)
by A54, A56, FINSEQ_4:26;
then A61:
j9 in Seg (len (decomp (((decomp b) /. i9) /. 2)))
by A59, FINSEQ_1:def 3;
A62:
(decomp (b12 + b2)) /. j9 = (decomp (b12 + b2)) . j9
by A54, PARTFUN1:def 8;
set m =
(Sum (Card (g | (i9 -' 1)))) + j9;
A63:
(
(Sum (Card (g | (i9 -' 1)))) + j9 in dom (FlattenSeq g) &
(FlattenSeq g) . ((Sum (Card (g | (i9 -' 1)))) + j9) = (g . i9) . j9 )
by A2, A52, A60, Th33;
A64:
(g . i9) . j9 =
(((len (decomp (((decomp b) /. i9) /. 2))) |-> <*(((decomp b) /. i9) /. 1)*>) . j9) ^ ((decomp (((decomp b) /. i9) /. 2)) . j9)
by A58, A60, Def2M
.=
<*b11*> ^ <*b12,b2*>
by A55, A57, A61, A62, FUNCOP_1:13
.=
<*b11,b12,b2*>
by FINSEQ_1:60
;
(decomp (((decomp b) /. i) /. 1)) /. j = (decomp (((decomp b) /. i) /. 1)) . j
by A41, A44, PARTFUN1:def 8;
then (f . i) . j =
<*b11,b12*> ^ <*b2*>
by A41, A43, A49, A50, A45, Def2M
.=
<*b11,b12,b2*>
by FINSEQ_1:60
;
hence
y in rng (FlattenSeq g)
by A39, A42, A64, A63, FUNCT_1:def 5;
verum
end; assume
y in rng (FlattenSeq g)
;
y in rng (FlattenSeq f)then consider k being
set such that A65:
k in dom (FlattenSeq g)
and A66:
y = (FlattenSeq g) . k
by FUNCT_1:def 5;
reconsider k =
k as
Element of
NAT by A65;
consider i,
j being
Element of
NAT such that A67:
i in dom g
and A68:
j in dom (g . i)
and
k = (Sum (Card (g | (i -' 1)))) + j
and A69:
(g . i) . j = (FlattenSeq g) . k
by A65, Th32;
set ddbi1 =
decomp (((decomp b) /. i) /. 2);
A70:
g . i = ((len (decomp (((decomp b) /. i) /. 2))) |-> <*(((decomp b) /. i) /. 1)*>) ^^ (decomp (((decomp b) /. i) /. 2))
by A4, A67;
then A71:
dom (g . i) =
(dom (decomp (((decomp b) /. i) /. 2))) /\ (dom ((len (decomp (((decomp b) /. i) /. 2))) |-> <*(((decomp b) /. i) /. 1)*>))
by Def2M
.=
(dom (decomp (((decomp b) /. i) /. 2))) /\ (Seg (len (decomp (((decomp b) /. i) /. 2))))
by FUNCOP_1:19
.=
(dom (decomp (((decomp b) /. i) /. 2))) /\ (dom (decomp (((decomp b) /. i) /. 2)))
by FINSEQ_1:def 3
.=
dom (decomp (((decomp b) /. i) /. 2))
;
dom (decomp (((decomp b) /. i) /. 2)) = Seg (len (decomp (((decomp b) /. i) /. 2)))
by FINSEQ_1:def 3;
then A72:
((len (decomp (((decomp b) /. i) /. 2))) |-> <*(((decomp b) /. i) /. 1)*>) . j = <*(((decomp b) /. i) /. 1)*>
by A68, A71, FUNCOP_1:13;
consider b1,
b2 being
bag of
n such that A73:
(decomp b) /. i = <*b1,b2*>
and A74:
b = b1 + b2
by A2, A67, Th72;
reconsider b19 =
b1,
b29 =
b2 as
Element of
Bags n by Def14;
A75:
(
b19 = b1 &
b29 = b2 )
;
then A76:
((decomp b) /. i) /. 1
= b1
by A73, FINSEQ_4:26;
((decomp b) /. i) /. 2
= b2
by A73, A75, FINSEQ_4:26;
then consider b11,
b12 being
bag of
n such that A77:
(decomp (((decomp b) /. i) /. 2)) /. j = <*b11,b12*>
and A78:
b2 = b11 + b12
by A68, A71, Th72;
(decomp (((decomp b) /. i) /. 2)) /. j = (decomp (((decomp b) /. i) /. 2)) . j
by A68, A71, PARTFUN1:def 8;
then A79:
(g . i) . j =
<*b1*> ^ <*b11,b12*>
by A68, A70, A76, A77, A72, Def2M
.=
<*b1,b11,b12*>
by FINSEQ_1:60
;
set b3 =
b1 + b11;
reconsider b39 =
b1 + b11,
b129 =
b12 as
Element of
Bags n by Def14;
consider j9 being
Element of
NAT such that A80:
j9 in dom (decomp (b1 + b11))
and A81:
(decomp (b1 + b11)) /. j9 = <*b1,b11*>
by Th73;
A82:
(decomp (b1 + b11)) /. j9 = (decomp (b1 + b11)) . j9
by A80, PARTFUN1:def 8;
b = (b1 + b11) + b12
by A74, A78, Th39;
then consider i9 being
Element of
NAT such that A83:
i9 in dom (decomp b)
and A84:
(decomp b) /. i9 = <*(b1 + b11),b12*>
by Th73;
set ddbi92 =
decomp (((decomp b) /. i9) /. 1);
set m =
(Sum (Card (f | (i9 -' 1)))) + j9;
A85:
(decomp b) /. i9 = <*b39,b129*>
by A84;
then A86:
((decomp b) /. i9) /. 1
= b1 + b11
by FINSEQ_4:26;
then A87:
j9 in Seg (len (decomp (((decomp b) /. i9) /. 1)))
by A80, FINSEQ_1:def 3;
A88:
f . i9 = (decomp (((decomp b) /. i9) /. 1)) ^^ ((len (decomp (((decomp b) /. i9) /. 1))) |-> <*(((decomp b) /. i9) /. 2)*>)
by A1, A3, A83;
then A89:
dom (f . i9) =
(dom ((len (decomp (((decomp b) /. i9) /. 1))) |-> <*(((decomp b) /. i9) /. 2)*>)) /\ (dom (decomp (((decomp b) /. i9) /. 1)))
by Def2M
.=
(Seg (len (decomp (((decomp b) /. i9) /. 1)))) /\ (dom (decomp (((decomp b) /. i9) /. 1)))
by FUNCOP_1:19
.=
(dom (decomp (((decomp b) /. i9) /. 1))) /\ (dom (decomp (((decomp b) /. i9) /. 1)))
by FINSEQ_1:def 3
.=
dom (decomp (((decomp b) /. i9) /. 1))
;
then A90:
(
(Sum (Card (f | (i9 -' 1)))) + j9 in dom (FlattenSeq f) &
(FlattenSeq f) . ((Sum (Card (f | (i9 -' 1)))) + j9) = (f . i9) . j9 )
by A1, A83, A80, A86, Th33;
A91:
((decomp b) /. i9) /. 2
= b12
by A85, FINSEQ_4:26;
(f . i9) . j9 =
((decomp (((decomp b) /. i9) /. 1)) . j9) ^ (((len (decomp (((decomp b) /. i9) /. 1))) |-> <*(((decomp b) /. i9) /. 2)*>) . j9)
by A80, A88, A86, A89, Def2M
.=
<*b1,b11*> ^ <*b12*>
by A81, A91, A86, A87, A82, FUNCOP_1:13
.=
<*b1,b11,b12*>
by FINSEQ_1:60
;
hence
y in rng (FlattenSeq f)
by A66, A69, A79, A90, FUNCT_1:def 5;
verum end;
then A92:
rng (FlattenSeq f) = rng (FlattenSeq g)
by TARSKI:2;
FlattenSeq f is one-to-one
proof
let k1,
k2 be
set ;
FUNCT_1:def 8 ( not k1 in proj1 (FlattenSeq f) or not k2 in proj1 (FlattenSeq f) or not (FlattenSeq f) . k1 = (FlattenSeq f) . k2 or k1 = k2 )
assume that A93:
k1 in dom (FlattenSeq f)
and A94:
k2 in dom (FlattenSeq f)
and A95:
(FlattenSeq f) . k1 = (FlattenSeq f) . k2
;
k1 = k2
consider i1,
j1 being
Element of
NAT such that A96:
i1 in dom f
and A97:
j1 in dom (f . i1)
and A98:
k1 = (Sum (Card (f | (i1 -' 1)))) + j1
and A99:
(f . i1) . j1 = (FlattenSeq f) . k1
by A93, Th32;
set ddbi11 =
decomp (((decomp b) /. i1) /. 1);
A100:
f . i1 = (decomp (((decomp b) /. i1) /. 1)) ^^ ((len (decomp (((decomp b) /. i1) /. 1))) |-> <*(((decomp b) /. i1) /. 2)*>)
by A3, A96;
then A101:
dom (f . i1) =
(dom (decomp (((decomp b) /. i1) /. 1))) /\ (dom ((len (decomp (((decomp b) /. i1) /. 1))) |-> <*(((decomp b) /. i1) /. 2)*>))
by Def2M
.=
(dom (decomp (((decomp b) /. i1) /. 1))) /\ (Seg (len (decomp (((decomp b) /. i1) /. 1))))
by FUNCOP_1:19
.=
(dom (decomp (((decomp b) /. i1) /. 1))) /\ (dom (decomp (((decomp b) /. i1) /. 1)))
by FINSEQ_1:def 3
.=
dom (decomp (((decomp b) /. i1) /. 1))
;
then A102:
(decomp (((decomp b) /. i1) /. 1)) /. j1 = (decomp (((decomp b) /. i1) /. 1)) . j1
by A97, PARTFUN1:def 8;
dom (decomp (((decomp b) /. i1) /. 1)) = Seg (len (decomp (((decomp b) /. i1) /. 1)))
by FINSEQ_1:def 3;
then A103:
((len (decomp (((decomp b) /. i1) /. 1))) |-> <*(((decomp b) /. i1) /. 2)*>) . j1 = <*(((decomp b) /. i1) /. 2)*>
by A97, A101, FUNCOP_1:13;
consider b11,
b12 being
bag of
n such that A104:
(decomp b) /. i1 = <*b11,b12*>
and
b = b11 + b12
by A1, A96, Th72;
reconsider b119 =
b11,
b129 =
b12 as
Element of
Bags n by Def14;
A105:
(
b119 = b11 &
b129 = b12 )
;
then
((decomp b) /. i1) /. 1
= b11
by A104, FINSEQ_4:26;
then consider b111,
b112 being
bag of
n such that A106:
(decomp (((decomp b) /. i1) /. 1)) /. j1 = <*b111,b112*>
and A107:
b11 = b111 + b112
by A97, A101, Th72;
((decomp b) /. i1) /. 2
= b12
by A104, A105, FINSEQ_4:26;
then A108:
(f . i1) . j1 =
<*b111,b112*> ^ <*b12*>
by A97, A100, A106, A102, A103, Def2M
.=
<*b111,b112,b12*>
by FINSEQ_1:60
;
consider i2,
j2 being
Element of
NAT such that A109:
i2 in dom f
and A110:
j2 in dom (f . i2)
and A111:
k2 = (Sum (Card (f | (i2 -' 1)))) + j2
and A112:
(f . i2) . j2 = (FlattenSeq f) . k2
by A94, Th32;
set ddbi21 =
decomp (((decomp b) /. i2) /. 1);
A113:
f . i2 = (decomp (((decomp b) /. i2) /. 1)) ^^ ((len (decomp (((decomp b) /. i2) /. 1))) |-> <*(((decomp b) /. i2) /. 2)*>)
by A3, A109;
then A114:
dom (f . i2) =
(dom (decomp (((decomp b) /. i2) /. 1))) /\ (dom ((len (decomp (((decomp b) /. i2) /. 1))) |-> <*(((decomp b) /. i2) /. 2)*>))
by Def2M
.=
(dom (decomp (((decomp b) /. i2) /. 1))) /\ (Seg (len (decomp (((decomp b) /. i2) /. 1))))
by FUNCOP_1:19
.=
(dom (decomp (((decomp b) /. i2) /. 1))) /\ (dom (decomp (((decomp b) /. i2) /. 1)))
by FINSEQ_1:def 3
.=
dom (decomp (((decomp b) /. i2) /. 1))
;
then A115:
(decomp (((decomp b) /. i2) /. 1)) /. j2 = (decomp (((decomp b) /. i2) /. 1)) . j2
by A110, PARTFUN1:def 8;
dom (decomp (((decomp b) /. i2) /. 1)) = Seg (len (decomp (((decomp b) /. i2) /. 1)))
by FINSEQ_1:def 3;
then A116:
((len (decomp (((decomp b) /. i2) /. 1))) |-> <*(((decomp b) /. i2) /. 2)*>) . j2 = <*(((decomp b) /. i2) /. 2)*>
by A110, A114, FUNCOP_1:13;
consider b21,
b22 being
bag of
n such that A117:
(decomp b) /. i2 = <*b21,b22*>
and
b = b21 + b22
by A1, A109, Th72;
reconsider b219 =
b21,
b229 =
b22 as
Element of
Bags n by Def14;
A118:
(
b219 = b21 &
b229 = b22 )
;
then
((decomp b) /. i2) /. 1
= b21
by A117, FINSEQ_4:26;
then consider b211,
b212 being
bag of
n such that A119:
(decomp (((decomp b) /. i2) /. 1)) /. j2 = <*b211,b212*>
and A120:
b21 = b211 + b212
by A110, A114, Th72;
((decomp b) /. i2) /. 2
= b22
by A117, A118, FINSEQ_4:26;
then A121:
(f . i2) . j2 =
<*b211,b212*> ^ <*b22*>
by A110, A113, A119, A115, A116, Def2M
.=
<*b211,b212,b22*>
by FINSEQ_1:60
;
then A122:
(
b111 = b211 &
b112 = b212 )
by A95, A99, A112, A108, FINSEQ_1:99;
A123:
(decomp b) /. i2 = (decomp b) . i2
by A1, A109, PARTFUN1:def 8;
A124:
(decomp b) /. i1 = (decomp b) . i1
by A1, A96, PARTFUN1:def 8;
b12 = b22
by A95, A99, A112, A108, A121, FINSEQ_1:99;
then
i1 = i2
by A1, A96, A109, A124, A104, A107, A123, A117, A120, A122, FUNCT_1:def 8;
hence
k1 = k2
by A97, A98, A110, A111, A106, A102, A114, A119, A115, A122, FUNCT_1:def 8;
verum
end;
then
FlattenSeq f, FlattenSeq g are_fiberwise_equipotent
by A92, A5, RFINSEQ:39;
hence
ex p being Permutation of (dom (FlattenSeq f)) st FlattenSeq g = (FlattenSeq f) * p
by RFINSEQ:17; verum