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 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]
proof
let i be Nat; :: thesis: ( S1[i] implies S1[i + 1] )
assume A5: S1[i] ; :: thesis: S1[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 S1[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