let X be set ; :: thesis:
let Y be finite Subset-Family of X; :: thesis:
let A, B be set ; :: thesis:
assume that
A1: A in Components Y and
A2: B in Components Y and
A3: A <> B ; :: thesis:
assume A /\ B <> {} ; :: according to XBOOLE_0:def 7 :: thesis:
then consider z being object such that
A4: z in A /\ B by XBOOLE_0:def 1;
A5: z in B by A4, XBOOLE_0:def 4;
A6: z in A by A4, XBOOLE_0:def 4;
consider p being FinSequence of bool X such that
len p = card Y and
rng p = Y and
A7: Components Y = { (Intersect (rng (MergeSequence (p,q)))) where q is FinSequence of BOOLEAN : len q = len p } by Def2;
consider q1 being FinSequence of BOOLEAN such that
A8: A = Intersect (rng (MergeSequence (p,q1))) and
len q1 = len p by A1, A7;
consider q2 being FinSequence of BOOLEAN such that
A9: B = Intersect (rng (MergeSequence (p,q2))) and
len q2 = len p by A2, A7;
A10: len (MergeSequence (p,q1)) = len p by Def1;
then A11: dom (MergeSequence (p,q1)) = Seg (len p) by FINSEQ_1:def 3;

A12: now :: thesis:

let i be Nat; :: thesis:
assume A13: i in dom (MergeSequence (p,q1)) ; :: thesis:
then A14: i in dom p by A11, FINSEQ_1:def 3;
(MergeSequence (p,q1)) . i in rng (MergeSequence (p,q1)) by A13, FUNCT_1:def 3;
then A15: z in (MergeSequence (p,q1)) . i by A8, A6, SETFAM_1:43;
i in dom (MergeSequence (p,q2)) by A14, Th1;
then (MergeSequence (p,q2)) . i in rng (MergeSequence (p,q2)) by FUNCT_1:def 3;
then A16: z in (MergeSequence (p,q2)) . i by A9, A5, SETFAM_1:43;

per cases by XBOOLEAN:def 3;

suppose q1 . i = TRUE ; :: thesis:

then A17: (MergeSequence (p,q1)) . i = p . i by Th2;
q2 . i = TRUE

assume not q2 . i = TRUE ; :: thesis:
then (MergeSequence (p,q2)) . i = X \ (p . i) by A14, Th3, XBOOLEAN:def 3;
hence contradiction by A15, A16, A17, XBOOLE_0:def 5; :: thesis:

end;

hence (MergeSequence (p,q1)) . i = (MergeSequence (p,q2)) . i by A17, Th2; :: thesis:

end;

suppose q1 . i = FALSE ; :: thesis:

then A18: (MergeSequence (p,q1)) . i = X \ (p . i) by A14, Th3;
q2 . i = FALSE

assume not q2 . i = FALSE ; :: thesis:
then q2 . i = TRUE by XBOOLEAN:def 3;
then (MergeSequence (p,q2)) . i = p . i by Th2;
hence contradiction by A15, A16, A18, XBOOLE_0:def 5; :: thesis:

end;

hence (MergeSequence (p,q1)) . i = (MergeSequence (p,q2)) . i by A14, A18, Th3; :: thesis:

end;

end;

end;

len (MergeSequence (p,q2)) = len p by Def1;
hence contradiction by A3, A8, A9, A10, A12, FINSEQ_2:9; :: thesis: