let X be set ; :: thesis: for Y being finite Subset-Family of X holds union (Components Y) = X
let Y be finite Subset-Family of X; :: thesis: union (Components Y) = X
X c= union (Components Y)

proof

deffunc H₁( set ) -> Element of BOOLEAN = FALSE ;
deffunc H₂( set ) -> Element of BOOLEAN = TRUE ;
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in X or z in union (Components Y) )
consider p being FinSequence of bool X such that
len p = card Y and
rng p = Y and
A1: Components Y = { (Intersect (rng (MergeSequence (p,q)))) where q is FinSequence of BOOLEAN : len q = len p } by Def2;
defpred S₁[ set ] means z in p . $1;
A2: for i being Nat st i in Seg (len p) holds
( ( S₁[i] implies H₂(i) in BOOLEAN ) & ( not S₁[i] implies H₁(i) in BOOLEAN ) ) ;
consider q being FinSequence of BOOLEAN such that
A3: len q = len p and
A4: for i being Nat st i in Seg (len p) holds
( ( S₁[i] implies q . i = H₂(i) ) & ( not S₁[i] implies q . i = H₁(i) ) ) from YELLOW15:sch 1(A2);
assume A5: z in X ; :: thesis: z in union (Components Y)

now :: thesis: for Z being set st Z in rng (MergeSequence (p,q)) holds
z in Z

let Z be set ; :: thesis: ( Z in rng (MergeSequence (p,q)) implies z in Z )
assume Z in rng (MergeSequence (p,q)) ; :: thesis: z in Z
then consider i being Nat such that
A6: i in dom (MergeSequence (p,q)) and
A7: (MergeSequence (p,q)) . i = Z by FINSEQ_2:10;
A8: dom (MergeSequence (p,q)) = dom p by Th1;
then A9: dom (MergeSequence (p,q)) = Seg (len p) by FINSEQ_1:def 3;

now :: thesis: z in Z

per cases ( z in p . i or not z in p . i ) ;

suppose A10: z in p . i ; :: thesis: z in Z

then q . i = TRUE by A4, A6, A9;
hence z in Z by A7, A10, Th2; :: thesis: verum

end;

suppose A11: not z in p . i ; :: thesis: z in Z

then q . i = FALSE by A4, A6, A9;
then (MergeSequence (p,q)) . i = X \ (p . i) by A6, A8, Th3;
hence z in Z by A5, A7, A11, XBOOLE_0:def 5; :: thesis: verum

end;

end;

end;

hence z in Z ; :: thesis: verum

end;

then A12: z in Intersect (rng (MergeSequence (p,q))) by A5, SETFAM_1:43;
Intersect (rng (MergeSequence (p,q))) in Components Y by A1, A3;
hence z in union (Components Y) by A12, TARSKI:def 4; :: thesis: verum

end;

hence union (Components Y) = X ; :: thesis: verum