let F be disjoint_valued FinSequence; :: thesis: for n, m being Nat st n < m holds
union (rng (F | n)) misses F . m
let n, m be Nat; :: thesis: ( n < m implies union (rng (F | n)) misses F . m )
assume A1: n < m ; :: thesis: union (rng (F | n)) misses F . m

per cases ( n >= len F or n < len F ) ;

suppose n >= len F ; :: thesis: union (rng (F | n)) misses F . m

then m > len F by A1, XXREAL_0:2;
then not m in dom F by FINSEQ_3:25;
then F . m = {} by FUNCT_1:def 2;
hence union (rng (F | n)) misses F . m ; :: thesis: verum

end;

suppose A2: n < len F ; :: thesis: union (rng (F | n)) misses F . m

for A being set st A in rng (F | n) holds
A misses F . m

proof

let A be set ; :: thesis: ( A in rng (F | n) implies A misses F . m )
assume A in rng (F | n) ; :: thesis: A misses F . m
then consider k being object such that
A3: ( k in dom (F | n) & A = (F | n) . k ) by FUNCT_1:def 3;
reconsider k = k as Element of NAT by A3;
( 1 <= k & k <= len (F | n) ) by A3, FINSEQ_3:25;
then A4: k <= n by A2, FINSEQ_1:59;
then A = F . k by A3, FINSEQ_3:112;
hence A misses F . m by A1, A4, PROB_2:def 2; :: thesis: verum

end;

hence union (rng (F | n)) misses F . m by ZFMISC_1:80; :: thesis: verum

end;

end;