let p1, p2 be Bags the carrier of R -valued FinSequence; :: thesis: ( 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 ) ) ) ; :: thesis: ( 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 ) ) ) ; :: thesis: p1 = p2
defpred S₁[ Nat] means ( G1 . $1 = G2 . $1 & F1 . $1 = F2 . $1 );
A3: S₁[ 0 ] by A1, A2;
A4: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A5: S₁[i] ; :: thesis: S₁[i + 1]
hence G1 . (i + 1) = (F2 . i) | { x where x is Element of R : x is_maximal_in support (F2 . i) } by A1
.= G2 . (i + 1) by A2 ;
:: thesis: F1 . (i + 1) = F2 . (i + 1)
hence F1 . (i + 1) = (F2 . i) -' (G2 . (i + 1)) by A1, A5
.= F2 . (i + 1) by A2 ;
:: thesis: verum

end;

A6: for i being Nat holds S₁[i] from NAT_1:sch 2(A3, A4);
A7: F1 = F2

proof

let i be Element of NAT ; :: according to PBOOLE:def 21 :: thesis: F1 . i = F2 . i
thus F1 . i = F2 . i by A6; :: thesis: verum

end;

A8: G1 = G2

proof

let i be Element of NAT ; :: according to PBOOLE:def 21 :: thesis: G1 . i = G2 . i
thus G1 . i = G2 . i by A6; :: thesis: verum

end;

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; :: thesis: verum