let X be set ; :: thesis: for S being non empty cap-closed semi-diff-closed Subset-Family of X
for E1, E2 being Element of S ex F1, F2, F3 being disjoint_valued FinSequence of S st
( union (rng F1) = E1 \ E2 & union (rng F2) = E2 \ E1 & union (rng F3) = E1 /\ E2 & (F1 ^ F2) ^ F3 is disjoint_valued FinSequence of S )
let S be non empty cap-closed semi-diff-closed Subset-Family of X; :: thesis: for E1, E2 being Element of S ex F1, F2, F3 being disjoint_valued FinSequence of S st
( union (rng F1) = E1 \ E2 & union (rng F2) = E2 \ E1 & union (rng F3) = E1 /\ E2 & (F1 ^ F2) ^ F3 is disjoint_valued FinSequence of S )
let E1, E2 be Element of S; :: thesis: ex F1, F2, F3 being disjoint_valued FinSequence of S st
( union (rng F1) = E1 \ E2 & union (rng F2) = E2 \ E1 & union (rng F3) = E1 /\ E2 & (F1 ^ F2) ^ F3 is disjoint_valued FinSequence of S )
consider F1 being disjoint_valued FinSequence of S such that
A2: E1 \ E2 = Union F1 by SRINGS_3:def 1;
consider F2 being disjoint_valued FinSequence of S such that
A3: E2 \ E1 = Union F2 by SRINGS_3:def 1;
E1 \ E2 misses E2 \ E1 by XBOOLE_1:82;
then union (rng F1) misses Union F2 by A2, A3, CARD_3:def 4;
then union (rng F1) misses union (rng F2) by CARD_3:def 4;
then reconsider G = F1 ^ F2 as disjoint_valued FinSequence of S by Th07;
rng G = (rng F1) \/ (rng F2) by FINSEQ_1:31;
then A4: union (rng G) = (union (rng F1)) \/ (union (rng F2)) by ZFMISC_1:78;
( Union F1 = union (rng F1) & Union F2 = union (rng F2) ) by CARD_3:def 4;
then Union G = (E1 \ E2) \/ (E2 \ E1) by A2, A3, A4, CARD_3:def 4;
then A5: Union G = E1 \+\ E2 by XBOOLE_0:def 6;
reconsider E = E1 /\ E2 as Element of S by FINSUB_1:def 2;
reconsider F3 = <*E*> as FinSequence of S ;
reconsider F3 = F3 as disjoint_valued FinSequence of S ;
take F1 ; :: thesis: ex F2, F3 being disjoint_valued FinSequence of S st
( union (rng F1) = E1 \ E2 & union (rng F2) = E2 \ E1 & union (rng F3) = E1 /\ E2 & (F1 ^ F2) ^ F3 is disjoint_valued FinSequence of S )
take F2 ; :: thesis: ex F3 being disjoint_valued FinSequence of S st
( union (rng F1) = E1 \ E2 & union (rng F2) = E2 \ E1 & union (rng F3) = E1 /\ E2 & (F1 ^ F2) ^ F3 is disjoint_valued FinSequence of S )
take F3 ; :: thesis: ( union (rng F1) = E1 \ E2 & union (rng F2) = E2 \ E1 & union (rng F3) = E1 /\ E2 & (F1 ^ F2) ^ F3 is disjoint_valued FinSequence of S )
reconsider F = G ^ <*E*> as FinSequence of S ;
thus ( union (rng F1) = E1 \ E2 & union (rng F2) = E2 \ E1 ) by A2, A3, CARD_3:def 4; :: thesis: ( union (rng F3) = E1 /\ E2 & (F1 ^ F2) ^ F3 is disjoint_valued FinSequence of S )
rng F3 = {E} by FINSEQ_1:38;
hence union (rng F3) = E1 /\ E2 by ZFMISC_1:25; :: thesis: (F1 ^ F2) ^ F3 is disjoint_valued FinSequence of S
A6: Union G misses E by A5, XBOOLE_1:103;
B1: len F = (len G) + 1 by FINSEQ_2:16;

A7: now :: thesis: for i, j being Nat st i in dom G & j = len F holds
F . i misses F . j

let i, j be Nat; :: thesis: ( i in dom G & j = len F implies F . i misses F . j )
assume A8: ( i in dom G & j = len F ) ; :: thesis: F . i misses F . j
then A9: F . j = E by B1, FINSEQ_1:42;
F . i = G . i by A8, FINSEQ_1:def 7;
then F . i c= union (rng G) by A8, FUNCT_1:3, ZFMISC_1:74;
then F . i c= Union G by CARD_3:def 4;
hence F . i misses F . j by A6, A9, XBOOLE_1:63; :: thesis: verum

end;

now :: thesis: for x, y being object st x <> y holds
F . x misses F . y

let x, y be object ; :: thesis: ( x <> y implies F . b₁ misses F . b₂ )
assume A10: x <> y ; :: thesis: F . b₁ misses F . b₂

per cases ( ( x in dom F & y in dom F ) or not x in dom F or not y in dom F ) ;

suppose A11: ( x in dom F & y in dom F ) ; :: thesis: F . b₁ misses F . b₂

then reconsider x1 = x, y1 = y as Nat ;
A12: ( 1 <= x1 & x1 <= len F & 1 <= y1 & y1 <= len F ) by A11, FINSEQ_3:25;

per cases ( x1 = len F or y1 = len F or ( x1 <> len F & y1 <> len F ) ) ;

suppose A13: x1 = len F ; :: thesis: F . b₁ misses F . b₂

then y1 < len F by A10, A12, XXREAL_0:1;
then y1 <= len G by B1, NAT_1:13;
hence F . x misses F . y by A7, A13, A12, FINSEQ_3:25; :: thesis: verum

end;

suppose A11: y1 = len F ; :: thesis: F . b₁ misses F . b₂

then x1 < len F by A10, A12, XXREAL_0:1;
then x1 <= len G by B1, NAT_1:13;
hence F . x misses F . y by A7, A11, A12, FINSEQ_3:25; :: thesis: verum

end;

suppose ( x1 <> len F & y1 <> len F ) ; :: thesis: F . b₁ misses F . b₂

then ( x1 < len F & y1 < len F ) by A12, XXREAL_0:1;
then ( x1 <= len G & y1 <= len G ) by B1, NAT_1:13;
then ( x1 in dom G & y1 in dom G ) by A12, FINSEQ_3:25;
then ( F . x = G . x & F . y = G . y ) by FINSEQ_1:def 7;
hence F . x misses F . y by A10, PROB_2:def 2; :: thesis: verum

end;

end;

end;

suppose ( not x in dom F or not y in dom F ) ; :: thesis: F . b₁ misses F . b₂

then ( F . x = {} or F . y = {} ) by FUNCT_1:def 2;
hence F . x misses F . y ; :: thesis: verum

end;

end;

end;

hence (F1 ^ F2) ^ F3 is disjoint_valued FinSequence of S by PROB_2:def 2; :: thesis: verum