set p = OrderedPartition b;
consider F, G being Function of NAT,(Bags the carrier of R) such that
A1: ( F . 0 = b & G . 0 = EmptyBag the carrier of R & ( for i being Nat holds
( G . (i + 1) = (F . i) | { x where x is Element of R : x is_maximal_in support (F . i) } & F . (i + 1) = (F . i) -' (G . (i + 1)) ) ) & ex i being Nat st
( F . i = EmptyBag the carrier of R & OrderedPartition b = G | (Seg i) & ( for j being Nat st j < i holds
F . j <> EmptyBag the carrier of R ) ) ) by OP;
consider i being Nat such that
A2: ( F . i = EmptyBag the carrier of R & OrderedPartition b = G | (Seg i) & ( for j being Nat st j < i holds
F . j <> EmptyBag the carrier of R ) ) by A1;
defpred S₁[ Nat] means ( $1 <= i implies b = (F . $1) + (Sum ((OrderedPartition b) | $1)) );
set I = the carrier of R;
A3: S₁[ 0 ]

proof

(OrderedPartition b) | 0 = <*> (Bags the carrier of R) ;
then Sum ((OrderedPartition b) | 0) = EmptyBag the carrier of R by Th21;
hence ( 0 <= i implies b = (F . 0) + (Sum ((OrderedPartition b) | 0)) ) by A1, PRE_POLY:53; :: thesis: verum

end;

dom G = NAT by FUNCT_2:def 1;
then ( dom (OrderedPartition b) = Seg i & i in NAT ) by A2, RELAT_1:62, ORDINAL1:def 12;
then A5: len (OrderedPartition b) = i by FINSEQ_1:def 3;
A4: for j being Nat st S₁[j] holds
S₁[j + 1]

proof

let j be Nat; :: thesis: ( S₁[j] implies S₁[j + 1] )
assume B1: ( S₁[j] & j + 1 <= i ) ; :: thesis: b = (F . (j + 1)) + (Sum ((OrderedPartition b) | (j + 1)))
rng (OrderedPartition b) c= Bags the carrier of R by RELAT_1:def 19;
then reconsider q = OrderedPartition b as FinSequence of Bags the carrier of R by FINSEQ_1:def 4;
B2: q | (j + 1) = (q | j) ^ <*(q /. (j + 1))*> by B1, A5, FINSEQ_5:82;
j + 1 in dom (OrderedPartition b) by A5, B1, NAT_1:11, FINSEQ_3:25;
then B4: ( q /. (j + 1) = (OrderedPartition b) . (j + 1) & (OrderedPartition b) . (j + 1) = G . (j + 1) ) by A2, PARTFUN1:def 6, FUNCT_1:47;
G . (j + 1) = (F . j) | { x where x is Element of R : x is_maximal_in support (F . j) } by A1;
then ( F . (j + 1) = (F . j) -' (G . (j + 1)) & G . (j + 1) divides F . j ) by A1, Th43;
then (F . (j + 1)) + (G . (j + 1)) = F . j by PRE_POLY:47;
hence b = (F . (j + 1)) + ((G . (j + 1)) + (Sum ((OrderedPartition b) | j))) by B1, NAT_1:13, RFUNCT_1:8
.= (F . (j + 1)) + (Sum ((OrderedPartition b) | (j + 1))) by B2, B4, Th22 ;
:: thesis: verum

end;

for j being Nat holds S₁[j] from NAT_1:sch 2(A3, A4);
then ( S₁[ len (OrderedPartition b)] & (OrderedPartition b) | (len (OrderedPartition b)) = OrderedPartition b ) by FINSEQ_1:58;
hence b = Sum (OrderedPartition b) by A2, A5, PRE_POLY:53; :: according to BAGORD_2:def 8 :: thesis: verum