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
consider p being FinSequence of bool X such that
len p = card Y and
rng p = Y and
A4: 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
A5: A = Intersect (rng (MergeSequence p,q1)) and
len q1 = len p by A1, A4;
consider q2 being FinSequence of BOOLEAN such that
A6: B = Intersect (rng (MergeSequence p,q2)) and
len q2 = len p by A2, A4;
assume A /\ B <> {} ; :: according to XBOOLE_0:def 7 :: thesis: contradiction
then consider z being set such that
A7: z in A /\ B by XBOOLE_0:def 1;
A8: ( z in A & z in B ) by A7, XBOOLE_0:def 4;
A9: ( len (MergeSequence p,q1) = len p & len (MergeSequence p,q2) = len p ) by Def1;
then X: dom (MergeSequence p,q1) = Seg (len p) by FINSEQ_1:def 3;

now

let i be Nat; :: thesis: ( i in dom (MergeSequence p,q1) implies (MergeSequence p,q1) . i = (MergeSequence p,q2) . i )
assume i in dom (MergeSequence p,q1) ; :: thesis: (MergeSequence p,q1) . i = (MergeSequence p,q2) . i
then A10: i in dom p by X, FINSEQ_1:def 3;
then ( i in dom (MergeSequence p,q1) & i in dom (MergeSequence p,q2) ) by Th5;
then ( (MergeSequence p,q1) . i in rng (MergeSequence p,q1) & (MergeSequence p,q2) . i in rng (MergeSequence p,q2) ) by FUNCT_1:def 5;
then A11: ( z in (MergeSequence p,q1) . i & z in (MergeSequence p,q2) . i ) by A5, A6, A8, SETFAM_1:58;

now

per cases ( q1 . i = TRUE or not q1 . i = TRUE ) ;

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

then A12: (MergeSequence p,q1) . i = p . i by Th6;
q2 . i = TRUE

proof

assume not q2 . i = TRUE ; :: thesis: contradiction
then q2 . i = FALSE by XBOOLEAN:def 3;
then (MergeSequence p,q2) . i = X \ (p . i) by A10, Th7;
hence contradiction by A11, A12, XBOOLE_0:def 5; :: thesis: verum

end;

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

end;

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

then q1 . i = FALSE by XBOOLEAN:def 3;
then A13: (MergeSequence p,q1) . i = X \ (p . i) by A10, Th7;
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 Th6;
hence contradiction by A11, A13, XBOOLE_0:def 5; :: thesis: verum

end;

hence (MergeSequence p,q1) . i = (MergeSequence p,q2) . i by A10, A13, Th7; :: thesis: verum

end;

end;

end;

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

end;

hence contradiction by A3, A5, A6, A9, FINSEQ_2:10; :: thesis: verum