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