let D be non empty set ; :: thesis: for Y being FinSequenceSet of D
for F being FinSequence of Y st ( for n, m being Nat st n <> m holds
union (rng (F . n)) misses union (rng (F . m)) ) & ( for n being Nat holds F . n is disjoint_valued ) holds
joined_FinSeq F is disjoint_valued
let Y be FinSequenceSet of D; :: thesis: for F being FinSequence of Y st ( for n, m being Nat st n <> m holds
union (rng (F . n)) misses union (rng (F . m)) ) & ( for n being Nat holds F . n is disjoint_valued ) holds
joined_FinSeq F is disjoint_valued
let F be FinSequence of Y; :: thesis: ( ( for n, m being Nat st n <> m holds
union (rng (F . n)) misses union (rng (F . m)) ) & ( for n being Nat holds F . n is disjoint_valued ) implies joined_FinSeq F is disjoint_valued )
assume that
A1: for n, m being Nat st n <> m holds
union (rng (F . n)) misses union (rng (F . m)) and
A2: for n being Nat holds F . n is disjoint_valued ; :: thesis: joined_FinSeq F is disjoint_valued

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

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

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

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

then reconsider n1 = x, n2 = y as Nat ;
consider k1, m1 being Nat such that
A5: ( 1 <= m1 & m1 <= len (F . (k1 + 1)) & k1 < len F & m1 + (Sum (Length (F | k1))) = n1 & n1 <= Sum (Length (F | (k1 + 1))) & (joined_FinSeq F) . x = (F . (k1 + 1)) . m1 ) by A4, Def2;
consider k2, m2 being Nat such that
A6: ( 1 <= m2 & m2 <= len (F . (k2 + 1)) & k2 < len F & m2 + (Sum (Length (F | k2))) = n2 & n2 <= Sum (Length (F | (k2 + 1))) & (joined_FinSeq F) . y = (F . (k2 + 1)) . m2 ) by A4, Def2;
( m1 in dom (F . (k1 + 1)) & m2 in dom (F . (k2 + 1)) ) by A5, A6, FINSEQ_3:25;
then A8: ( (joined_FinSeq F) . x in rng (F . (k1 + 1)) & (joined_FinSeq F) . y in rng (F . (k2 + 1)) ) by A5, A6, FUNCT_1:3;

now :: thesis: (joined_FinSeq F) . x misses (joined_FinSeq F) . y

assume A9: not (joined_FinSeq F) . x misses (joined_FinSeq F) . y ; :: thesis: contradiction
then ((joined_FinSeq F) . x) /\ ((joined_FinSeq F) . y) <> {} by XBOOLE_0:def 7;
then consider z being object such that
A10: z in ((joined_FinSeq F) . x) /\ ((joined_FinSeq F) . y) by XBOOLE_0:def 1;
( z in (joined_FinSeq F) . x & z in (joined_FinSeq F) . y ) by A10, XBOOLE_0:def 4;
then ( z in union (rng (F . (k1 + 1))) & z in union (rng (F . (k2 + 1))) ) by A8, TARSKI:def 4;
then A11: k1 + 1 = k2 + 1 by A1, XBOOLE_0:3;
F . (k1 + 1) is disjoint_valued by A2;
hence contradiction by A5, A6, A3, A9, A11, PROB_2:def 2; :: thesis: verum

end;

hence (joined_FinSeq F) . x misses (joined_FinSeq F) . y ; :: thesis: verum

end;

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

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

end;

end;

end;

hence joined_FinSeq F is disjoint_valued by PROB_2:def 2; :: thesis: verum