let e be set ; :: thesis: ( e in (bool (the_universe_of (X \/ NAT ))) ^omega implies ex u being set st S₁[e,u] )
assume e in (bool (the_universe_of (X \/ NAT ))) ^omega ; :: thesis: ex u being set st S₁[e,u]
then reconsider fs = e as XFinSequence of bool (the_universe_of (X \/ NAT )) by AFINSQ_1:def 8;
( dom fs = 0 or (dom fs) + 1 > 0 + 1 ) by XREAL_1:8;
then ( dom fs = 0 or dom fs >= 1 ) by NAT_1:13;
then ( dom fs = 0 or dom fs = 1 or dom fs > 1 ) by XXREAL_0:1;
then A2: ( dom fs = 0 or dom fs = 1 or (dom fs) + 1 > 1 + 1 ) by XREAL_1:8;

per cases ( dom fs = 0 or dom fs = 1 or dom fs >= 2 ) by A2, NAT_1:13;

suppose A3: dom fs = 0 ; :: thesis: ex u being set st S₁[e,u]

set u = {} ;
take {} ; :: thesis: S₁[e, {} ]
thus S₁[e, {} ] by A3; :: thesis: verum

end;

suppose A4: dom fs = 1 ; :: thesis: ex u being set st S₁[e,u]

set u = X;
take X ; :: thesis: S₁[e,X]
thus S₁[e,X] by A4; :: thesis: verum

end;

suppose A5: dom fs >= 2 ; :: thesis: ex u being set st S₁[e,u]

reconsider n = dom fs as natural number ;
reconsider n9 = n -' 1 as Nat ;
n - 1 >= 2 - 1 by A5, XREAL_1:11;
then A6: n9 = n - 1 by XREAL_0:def 2;
defpred S₂[ set , set ] means for p being natural number st p >= 1 & p <= n - 1 & $1 = p holds
$2 = [:(fs . p),(fs . (n - p)):];
A7: for k being Nat st k in Seg n9 holds
ex x being set st S₂[k,x]

proof

let k be Nat; :: thesis: ( k in Seg n9 implies ex x being set st S₂[k,x] )
assume k in Seg n9 ; :: thesis: ex x being set st S₂[k,x]
set x = [:(fs . k),(fs . (n - k)):];
take [:(fs . k),(fs . (n - k)):] ; :: thesis: S₂[k,[:(fs . k),(fs . (n - k)):]]
thus S₂[k,[:(fs . k),(fs . (n - k)):]] ; :: thesis: verum

end;

consider fs1 being FinSequence such that
A8: ( dom fs1 = Seg n9 & ( for k being Nat st k in Seg n9 holds
S₂[k,fs1 . k] ) ) from FINSEQ_1:sch 1(A7);
set u = Union (disjoin fs1);
take Union (disjoin fs1) ; :: thesis: S₁[e, Union (disjoin fs1)]
A9: len fs1 = n - 1 by A6, A8, FINSEQ_1:def 3;
for p being natural number st p >= 1 & p <= n - 1 holds
fs1 . p = [:(fs . p),(fs . (n - p)):]

proof

let p be natural number ; :: thesis: ( p >= 1 & p <= n - 1 implies fs1 . p = [:(fs . p),(fs . (n - p)):] )
assume A10: ( p >= 1 & p <= n - 1 ) ; :: thesis: fs1 . p = [:(fs . p),(fs . (n - p)):]
then p in Seg n9 by A6, FINSEQ_1:3;
hence fs1 . p = [:(fs . p),(fs . (n - p)):] by A8, A10; :: thesis: verum

end;

hence S₁[e, Union (disjoin fs1)] by A5, A9; :: thesis: verum

end;

end;