theorem :: PRE_POLY:74

for n being 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