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