theorem Th13: :: REARRAN1:14

for C, D being non empty finite set
for c being Element of C
for F being PartFunc of D,REAL
for A being RearrangmentGen of C st F is total & card C = card D holds
( ( c in A . 1 implies ((MIM (FinS (F,D))) (#) (CHI (A,C))) # c = MIM (FinS (F,D)) ) & ( for n being Nat st 1 <= n & n < len A & c in (A . (n + 1)) \ (A . n) holds
((MIM (FinS (F,D))) (#) (CHI (A,C))) # c = (n |-> 0) ^ (MIM ((FinS (F,D)) /^ n)) ) )