let f be Function; :: thesis: for n being Nat holds (union (rng (f | n))) \/ (f . n) = union (rng (f | (n + 1)))
let n be Nat; :: thesis: (union (rng (f | n))) \/ (f . n) = union (rng (f | (n + 1)))
thus (union (rng (f | n))) \/ (f . n) 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)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (union (rng (f | n))) \/ (f . n) or x in union (rng (f | (n + 1))) )
assume A1: x in (union (rng (f | n))) \/ (f . n) ; :: thesis: x in union (rng (f | (n + 1)))

now :: thesis: x in union (rng (f | (n + 1)))

per cases ( x in union (rng (f | n)) or x in f . n ) by A1, XBOOLE_0:def 3;

suppose x in union (rng (f | n)) ; :: thesis: x in union (rng (f | (n + 1)))

then consider Y being set such that
A2: x in Y and
A3: Y in rng (f | n) by TARSKI:def 4;
consider X being object such that
A4: X in dom (f | n) and
A5: (f | n) . X = Y by A3, FUNCT_1:def 3;
A6: (f | n) . X = f . X by A4, FUNCT_1:47;
n <= n + 1 by NAT_1:11;
then Segm n c= Segm (n + 1) by NAT_1:39;
then A7: (dom f) /\ n c= (dom f) /\ (n + 1) by XBOOLE_1:26;
X in (dom f) /\ n by A4, RELAT_1:61;
then X in (dom f) /\ (n + 1) by A7;
then A8: X in dom (f | (n + 1)) by RELAT_1:61;
then A9: (f | (n + 1)) . X = f . X by FUNCT_1:47;
(f | (n + 1)) . X in rng (f | (n + 1)) by A8, FUNCT_1:def 3;
hence x in union (rng (f | (n + 1))) by A2, A5, A9, A6, TARSKI:def 4; :: thesis: verum

end;

suppose A10: x in f . n ; :: thesis: x in union (rng (f | (n + 1)))

n < n + 1 by NAT_1:13;
then A11: n in Segm (n + 1) by NAT_1:44;
n in dom f by A10, FUNCT_1:def 2;
then n in (dom f) /\ (n + 1) by A11, XBOOLE_0:def 4;
then A12: n in dom (f | (n + 1)) by RELAT_1:61;
then A13: (f | (n + 1)) . n = f . n by FUNCT_1:47;
(f | (n + 1)) . n in rng (f | (n + 1)) by A12, FUNCT_1:def 3;
hence x in union (rng (f | (n + 1))) by A10, A13, TARSKI:def 4; :: thesis: verum

end;

end;

end;

hence x in union (rng (f | (n + 1))) ; :: thesis: verum

end;

thus union (rng (f | (n + 1))) c= (union (rng (f | n))) \/ (f . n) :: thesis: verum

proof

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) )
assume x in union (rng (f | (n + 1))) ; :: thesis: x in (union (rng (f | n))) \/ (f . n)
then consider Y being set such that
A14: x in Y and
A15: Y in rng (f | (n + 1)) by TARSKI:def 4;
consider X being object such that
A16: X in dom (f | (n + 1)) and
A17: (f | (n + 1)) . X = Y by A15, FUNCT_1:def 3;
A18: X in (dom f) /\ (n + 1) by A16, RELAT_1:61;
then A19: X in Segm (n + 1) by XBOOLE_0:def 4;
A20: X in dom f by A18, XBOOLE_0:def 4;
reconsider X = X as Element of NAT by A19;
X < n + 1 by A19, NAT_1:44;
then A21: X <= n by NAT_1:13;

now :: thesis: x in (union (rng (f | n))) \/ (f . n)

per cases ( X < n or X = n ) by A21, XXREAL_0:1;

suppose X < n ; :: thesis: x in (union (rng (f | n))) \/ (f . n)

then X in Segm n by NAT_1:44;
then X in (dom f) /\ n by A20, XBOOLE_0:def 4;
then A22: X in dom (f | n) by RELAT_1:61;
then A23: (f | n) . X in rng (f | n) by FUNCT_1:def 3;
A24: f . X = (f | (n + 1)) . X by A16, FUNCT_1:47;
(f | n) . X = f . X by A22, FUNCT_1:47;
then x in union (rng (f | n)) by A14, A17, A24, A23, TARSKI:def 4;
hence x in (union (rng (f | n))) \/ (f . n) by XBOOLE_0:def 3; :: thesis: verum

end;

suppose A25: X = n ; :: thesis: x in (union (rng (f | n))) \/ (f . n)

f . X = (f | (n + 1)) . X by A16, FUNCT_1:47;
hence x in (union (rng (f | n))) \/ (f . n) by A14, A17, A25, XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

hence x in (union (rng (f | n))) \/ (f . n) ; :: thesis: verum

end;