let F be FinSequence; :: thesis: for n being Nat holds (union (rng (F | n))) \/ (F . (n + 1)) = union (rng (F | (n + 1)))
let n be Nat; :: thesis: (union (rng (F | n))) \/ (F . (n + 1)) = union (rng (F | (n + 1)))

now :: thesis: for x being set st x in (union (rng (F | n))) \/ (F . (n + 1)) holds
x in union (rng (F | (n + 1)))

let x be set ; :: thesis: ( x in (union (rng (F | n))) \/ (F . (n + 1)) implies b₁ in union (rng (F | (n + 1))) )
assume x in (union (rng (F | n))) \/ (F . (n + 1)) ; :: thesis: b₁ in union (rng (F | (n + 1)))

per cases then ( x in union (rng (F | n)) or x in F . (n + 1) ) by XBOOLE_0:def 3;

suppose x in union (rng (F | n)) ; :: thesis: b₁ in union (rng (F | (n + 1)))

then consider A being set such that
A2: ( x in A & A in rng (F | n) ) by TARSKI:def 4;
consider k being object such that
A3: ( k in dom (F | n) & A = (F | n) . k ) by A2, FUNCT_1:def 3;
reconsider k = k as Element of NAT by A3;
A4: ( 1 <= k & k <= len (F | n) ) by A3, FINSEQ_3:25;
len (F | n) <= n by FINSEQ_1:86;
then A5: ( k <= n & A = F . k ) by A4, A3, FINSEQ_3:112, XXREAL_0:2;
n <= n + 1 by NAT_1:11;
then A6: A = (F | (n + 1)) . k by A5, XXREAL_0:2, FINSEQ_3:112;
len (F | n) <= len (F | (n + 1)) by NAT_1:11, Th73;
then k <= len (F | (n + 1)) by A4, XXREAL_0:2;
then k in dom (F | (n + 1)) by A4, FINSEQ_3:25;
then A in rng (F | (n + 1)) by A6, FUNCT_1:3;
hence x in union (rng (F | (n + 1))) by A2, TARSKI:def 4; :: thesis: verum

end;

suppose x in F . (n + 1) ; :: thesis: b₁ in union (rng (F | (n + 1)))

then A7: x in (F | (n + 1)) . (n + 1) by FINSEQ_3:112;
then n + 1 in dom (F | (n + 1)) by FUNCT_1:def 2;
then (F | (n + 1)) . (n + 1) in rng (F | (n + 1)) by FUNCT_1:3;
hence x in union (rng (F | (n + 1))) by A7, TARSKI:def 4; :: thesis: verum

end;

end;

end;

hence (union (rng (F | n))) \/ (F . (n + 1)) c= union (rng (F | (n + 1))) ; :: according to XBOOLE_0:def 10 :: thesis: union (rng (F | (n + 1))) c= (union (rng (F | n))) \/ (F . (n + 1))
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union (rng (F | (n + 1))) or x in (union (rng (F | n))) \/ (F . (n + 1)) )
assume x in union (rng (F | (n + 1))) ; :: thesis: x in (union (rng (F | n))) \/ (F . (n + 1))
then consider A being set such that
A9: ( x in A & A in rng (F | (n + 1)) ) by TARSKI:def 4;
consider k being object such that
A10: ( k in dom (F | (n + 1)) & A = (F | (n + 1)) . k ) by A9, FUNCT_1:def 3;
reconsider k = k as Element of NAT by A10;
( 1 <= k & k <= len (F | (n + 1)) & len (F | (n + 1)) <= n + 1 ) by A10, FINSEQ_1:86, FINSEQ_3:25;
then A11: ( k <= n + 1 & (F | (n + 1)) . k = F . k ) by XXREAL_0:2, FINSEQ_3:112;

per cases ( k = n + 1 or k <> n + 1 ) ;

suppose k = n + 1 ; :: thesis: x in (union (rng (F | n))) \/ (F . (n + 1))

hence x in (union (rng (F | n))) \/ (F . (n + 1)) by A9, A10, A11, XBOOLE_0:def 3; :: thesis: verum

end;

suppose k <> n + 1 ; :: thesis: x in (union (rng (F | n))) \/ (F . (n + 1))

then k < n + 1 by A11, XXREAL_0:1;
then k <= n by NAT_1:13;
then A12: (F | n) . k = F . k by FINSEQ_3:112;
then k in dom (F | n) by A11, A10, A9, FUNCT_1:def 2;
then A in rng (F | n) by A12, A11, A10, FUNCT_1:3;
then x in union (rng (F | n)) by A9, TARSKI:def 4;
hence x in (union (rng (F | n))) \/ (F . (n + 1)) by XBOOLE_0:def 3; :: thesis: verum

end;

end;