let F be disjoint_valued FinSequence; :: thesis: for n being Nat holds Union (F | n) misses F . (n + 1)
let n be Nat; :: thesis: Union (F | n) misses F . (n + 1)
assume Union (F | n) meets F . (n + 1) ; :: thesis: contradiction
then consider x being object such that
A1: ( x in Union (F | n) & x in F . (n + 1) ) by XBOOLE_0:3;
x in union (rng (F | n)) by A1, CARD_3:def 4;
then consider A being set such that
A2: ( x in A & A in rng (F | n) ) by TARSKI:def 4;
consider m being object such that
A3: ( m in dom (F | n) & A = (F | n) . m ) by A2, FUNCT_1:def 3;
reconsider m = m as Element of NAT by A3;
( m <= len (F | n) & len (F | n) <= n ) by A3, FINSEQ_3:25, FINSEQ_1:86;
then m <> n + 1 by NAT_1:13;
then F . m misses F . (n + 1) by PROB_2:def 2;
then ((F | n) . m) /\ (F . (n + 1)) = {} by A3, FUNCT_1:47;
hence contradiction by A1, A2, A3, XBOOLE_0:def 4; :: thesis: verum