set I = the carrier of R;
deffunc H1( bag of the carrier of R) -> set = { x where x is Element of R : x is_maximal_in support $1 } ;
deffunc H2( Nat, Element of [:(Bags the carrier of R),(Bags the carrier of R):]) -> Element of [:(Bags the carrier of R),(Bags the carrier of R):] = [(($2 `1) -' (($2 `1) | H1($2 `1 ))),(($2 `1) | H1($2 `1 ))];
consider f being Function of NAT,[:(Bags the carrier of R),(Bags the carrier of R):] such that
A1: ( f . 0 = [b,(EmptyBag the carrier of R)] & ( for i being Nat holds f . (i + 1) = H2(i,f . i) ) ) from NAT_1:sch 12();
 defpred S1[ Nat] means ex i being Nat st card (support ((f . i) `1)) = $1;
defpred S2[ Nat] means card (support ((f . $1) `1)) = 0 ;
A2: ex k being Nat st S1[k]
proof
take k = card (support ((f . 0) `1)); :: thesis: S1[k]
take i = 0 ; :: thesis: card (support ((f . i) `1)) = k
thus card (support ((f . i) `1)) = k ; :: thesis: verum
end;
A3: for k being Nat st k <> 0 & S1[k] holds
ex n being Nat st
( n < k & S1[n] )
proof
let k be Nat; :: thesis: ( k <> 0 & S1[k] implies ex n being Nat st
( n < k & S1[n] ) )
assume Z0: k <> 0 ; :: thesis: ( not S1[k] or ex n being Nat st
( n < k & S1[n] ) )
given i being Nat such that Z1: card (support ((f . i) `1)) = k ; :: thesis: ex n being Nat st
( n < k & S1[n] )
(f . i) `1 <> EmptyBag the carrier of R by Z0, Z1;
then B1: H1((f . i) `1 ) <> {} by Th42;
f . (i + 1) = H2(i,f . i) by A1;
then B2: support ((f . (i + 1)) `1) = (support ((f . i) `1)) \ H1((f . i) `1 ) by Th27A;
H1((f . i) `1 ) c= support ((f . i) `1)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in H1((f . i) `1 ) or x in support ((f . i) `1) )
assume x in H1((f . i) `1 ) ; :: thesis: x in support ((f . i) `1)
then ex y being Element of R st
( x = y & y is_maximal_in support ((f . i) `1) ) ;
hence x in support ((f . i) `1) by WAYBEL_4:55; :: thesis: verum
end;
then reconsider S = H1((f . i) `1 ) as finite Subset of (support ((f . i) `1)) ;
take n = card (support ((f . (i + 1)) `1)); :: thesis: ( n < k & S1[n] )
card S <> 0 by B1;
then ( n = k - (card S) & card S > 0 ) by Z1, B2, CARD_2:44;
hence n < k by XREAL_1:44; :: thesis: S1[n]
thus S1[n] ; :: thesis: verum
end;
S1[ 0 ] from NAT_1:sch 7(A2, A3);
 then A4: ex i being Nat st S2[i] ;
consider i being Nat such that
A5: ( S2[i] & ( for n being Nat st S2[n] holds
i <= n ) ) from NAT_1:sch 5(A4);
 ( Seg i c= NAT & NAT = dom (pr2 f) ) by FUNCT_2:def 1;
then dom ((pr2 f) | (Seg i)) = Seg i by RELAT_1:62;
then reconsider p = (pr2 f) | (Seg i) as Bags the carrier of R -valued FinSequence by FINSEQ_1:def 2;
take p ; :: 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 & p = G | (Seg i) & ( for j being Nat st j < i holds
F . j <> EmptyBag the carrier of R ) ) )
take F = pr1 f; :: thesis: ex 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 & p = G | (Seg i) & ( for j being Nat st j < i holds
F . j <> EmptyBag the carrier of R ) ) )
take G = pr2 f; :: thesis: ( 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 & p = G | (Seg i) & ( for j being Nat st j < i holds
F . j <> EmptyBag the carrier of R ) ) )
thus F . 0 = (f . 0) `1 by FUNCT_2:def 5
.= b by A1 ; :: thesis: ( 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 & p = G | (Seg i) & ( for j being Nat st j < i holds
F . j <> EmptyBag the carrier of R ) ) )
thus G . 0 = (f . 0) `2 by FUNCT_2:def 6
.= EmptyBag the carrier of R by A1 ; :: thesis: ( ( 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 & p = G | (Seg i) & ( for j being Nat st j < i holds
F . j <> EmptyBag the carrier of R ) ) )
hereby :: thesis: ex i being Nat st
( F . i = EmptyBag the carrier of R & p = G | (Seg i) & ( for j being Nat st j < i holds
F . j <> EmptyBag the carrier of R ) )
let i be Nat; :: thesis: ( G . (i + 1) = (F . i) | H1(F . i) & F . (i + 1) = (F . i) -' (G . (i + 1)) )
reconsider j = i as Element of NAT by ORDINAL1:def 12;
A6: G . (i + 1) = (f . (i + 1)) `2 by FUNCT_2:def 6
.= H2(i,f . i) `2 by A1
.= ((f . j) `1) | H1((f . j) `1 ) ;
(f . j) `1 = F . i by FUNCT_2:def 5;
hence G . (i + 1) = (F . i) | H1(F . i) by A6; :: thesis: F . (i + 1) = (F . i) -' (G . (i + 1))
thus F . (i + 1) = (f . (i + 1)) `1 by FUNCT_2:def 5
.= H2(i,f . i) `1 by A1
.= ((f . j) `1) -' (G . (i + 1)) by A6
.= (F . i) -' (G . (i + 1)) by FUNCT_2:def 5 ; :: thesis: verum
end;
take i ; :: thesis: ( F . i = EmptyBag the carrier of R & p = G | (Seg i) & ( for j being Nat st j < i holds
F . j <> EmptyBag the carrier of R ) )
reconsider j = i as Element of NAT by ORDINAL1:def 12;
support ((f . i) `1) = {} by A5;
then (f . j) `1 = EmptyBag the carrier of R by PRE_POLY:81;
hence F . i = EmptyBag the carrier of R by FUNCT_2:def 5; :: thesis: ( p = G | (Seg i) & ( for j being Nat st j < i holds
F . j <> EmptyBag the carrier of R ) )
thus p = G | (Seg i) ; :: thesis: for j being Nat st j < i holds
F . j <> EmptyBag the carrier of R
let k be Nat; :: thesis: ( k < i implies F . k <> EmptyBag the carrier of R )
reconsider j = k as Element of NAT by ORDINAL1:def 12;
assume k < i ; :: thesis: F . k <> EmptyBag the carrier of R
then not S2[k] by A5;
then (f . j) `1 <> EmptyBag the carrier of R ;
hence F . k <> EmptyBag the carrier of R by FUNCT_2:def 5; :: thesis: verum