let X be set ; :: thesis: for Y being finite Subset-Family of X
for A, B being set st A in Components Y & B in Components Y & A <> B holds
A misses B
let Y be finite Subset-Family of X; :: thesis: for A, B being set st A in Components Y & B in Components Y & A <> B holds
A misses B
let A, B be set ; :: thesis: ( A in Components Y & B in Components Y & A <> B implies A misses B )
assume that
A1: A in Components Y and
A2: B in Components Y and
A3: A <> B ; :: thesis: A misses B
assume A /\ B <> {} ; :: according to XBOOLE_0:def 7 :: thesis: contradiction
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: for i being Nat st i in dom (MergeSequence (p,q1)) holds
(MergeSequence (p,q1)) . i = (MergeSequence (p,q2)) . i

let i be Nat; :: thesis: ( i in dom (MergeSequence (p,q1)) implies (MergeSequence (p,q1)) . b₁ = (MergeSequence (p,q2)) . b₁ )
assume A13: i in dom (MergeSequence (p,q1)) ; :: thesis: (MergeSequence (p,q1)) . b₁ = (MergeSequence (p,q2)) . b₁
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 ( q1 . i = TRUE or q1 . i = FALSE ) by XBOOLEAN:def 3;

suppose q1 . i = TRUE ; :: thesis: (MergeSequence (p,q1)) . b₁ = (MergeSequence (p,q2)) . b₁

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

proof

assume not q2 . i = TRUE ; :: thesis: contradiction
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: verum

end;

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

end;

suppose q1 . i = FALSE ; :: thesis: (MergeSequence (p,q1)) . b₁ = (MergeSequence (p,q2)) . b₁

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

proof

assume not q2 . i = FALSE ; :: thesis: contradiction
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: verum

end;

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

end;

end;

end;

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