let p1, p2 be Bags the carrier of R -valued FinSequence; ( ex F, G being Function of NAT,(Bags the carrier of R) st
( 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 & p1 = G | (Seg i) & ( for j being Nat st j < i holds
F . j <> EmptyBag the carrier of R ) ) ) & ex F, G being Function of NAT,(Bags the carrier of R) st
( 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 & p2 = G | (Seg i) & ( for j being Nat st j < i holds
F . j <> EmptyBag the carrier of R ) ) ) implies p1 = p2 )
given F1, G1 being Function of NAT,(Bags the carrier of R) such that A1:
( F1 . 0 = b & G1 . 0 = EmptyBag the carrier of R & ( for i being Nat holds
( G1 . (i + 1) = (F1 . i) | { x where x is Element of R : x is_maximal_in support (F1 . i) } & F1 . (i + 1) = (F1 . i) -' (G1 . (i + 1)) ) ) & ex i being Nat st
( F1 . i = EmptyBag the carrier of R & p1 = G1 | (Seg i) & ( for j being Nat st j < i holds
F1 . j <> EmptyBag the carrier of R ) ) )
; ( for F, G being Function of NAT,(Bags the carrier of R) holds
( not F . 0 = b or not G . 0 = EmptyBag the carrier of R or ex i being Nat st
( G . (i + 1) = (F . i) | { x where x is Element of R : x is_maximal_in support (F . i) } implies not F . (i + 1) = (F . i) -' (G . (i + 1)) ) or for i being Nat holds
( not F . i = EmptyBag the carrier of R or not p2 = G | (Seg i) or ex j being Nat st
( j < i & not F . j <> EmptyBag the carrier of R ) ) ) or p1 = p2 )
given F2, G2 being Function of NAT,(Bags the carrier of R) such that A2:
( F2 . 0 = b & G2 . 0 = EmptyBag the carrier of R & ( for i being Nat holds
( G2 . (i + 1) = (F2 . i) | { x where x is Element of R : x is_maximal_in support (F2 . i) } & F2 . (i + 1) = (F2 . i) -' (G2 . (i + 1)) ) ) & ex i being Nat st
( F2 . i = EmptyBag the carrier of R & p2 = G2 | (Seg i) & ( for j being Nat st j < i holds
F2 . j <> EmptyBag the carrier of R ) ) )
; p1 = p2
defpred S1[ Nat] means ( G1 . $1 = G2 . $1 & F1 . $1 = F2 . $1 );
A3:
S1[ 0 ]
by A1, A2;
A4:
for i being Nat st S1[i] holds
S1[i + 1]
A6:
for i being Nat holds S1[i]
from NAT_1:sch 2(A3, A4);
A7:
F1 = F2
A8:
G1 = G2
consider i1 being Nat such that
A9:
( F1 . i1 = EmptyBag the carrier of R & p1 = G1 | (Seg i1) & ( for j being Nat st j < i1 holds
F1 . j <> EmptyBag the carrier of R ) )
by A1;
consider i2 being Nat such that
AA:
( F1 . i2 = EmptyBag the carrier of R & p2 = G1 | (Seg i2) & ( for j being Nat st j < i2 holds
F1 . j <> EmptyBag the carrier of R ) )
by A2, A7, A8;
( i1 <= i2 & i2 <= i1 )
by A9, AA;
hence
p1 = p2
by A9, AA, XXREAL_0:1; verum