let D be non empty set ; :: thesis:
let Y be FinSequenceSet of D; :: thesis:
let F be FinSequence of Y; :: thesis:
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:

let x, y be object ; :: thesis:
assume A3: x <> y ; :: thesis:

suppose A4: ( x in dom (joined_FinSeq F) & y in dom (joined_FinSeq F) ) ; :: thesis:

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;

assume A9: not (joined_FinSeq F) . x misses (joined_FinSeq F) . y ; :: thesis:
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:

end;

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

end;

suppose ( not x in dom (joined_FinSeq F) or not y in dom (joined_FinSeq F) ) ; :: thesis:

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:

end;

end;

end;

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