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;

hence contradiction by A3, A8, A9, A10, A12, FINSEQ_2:9; :: thesis: verum

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

len (MergeSequence (p,q2)) = len p
by Def1;(MergeSequence (p,q1)) . i = (MergeSequence (p,q2)) . i

let i be Nat; :: thesis: ( i in dom (MergeSequence (p,q1)) implies (MergeSequence (p,q1)) . b_{1} = (MergeSequence (p,q2)) . b_{1} )

assume A13: i in dom (MergeSequence (p,q1)) ; :: thesis: (MergeSequence (p,q1)) . b_{1} = (MergeSequence (p,q2)) . b_{1}

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;

end;assume A13: i in dom (MergeSequence (p,q1)) ; :: thesis: (MergeSequence (p,q1)) . 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;

end;

suppose
q1 . i = TRUE
; :: thesis: (MergeSequence (p,q1)) . b_{1} = (MergeSequence (p,q2)) . b_{1}

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

q2 . i = TRUE

end;q2 . i = TRUE

proof

hence
(MergeSequence (p,q1)) . i = (MergeSequence (p,q2)) . i
by A17, Th2; :: thesis: verum
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;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

suppose
q1 . i = FALSE
; :: thesis: (MergeSequence (p,q1)) . b_{1} = (MergeSequence (p,q2)) . b_{1}

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

q2 . i = FALSE

end;q2 . i = FALSE

proof

hence
(MergeSequence (p,q1)) . i = (MergeSequence (p,q2)) . i
by A14, A18, Th3; :: thesis: verum
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;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

hence contradiction by A3, A8, A9, A10, A12, FINSEQ_2:9; :: thesis: verum