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)

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

thus
union (rng (f | (n + 1))) c= (union (rng (f | n))) \/ (f . n)
:: thesis: verum
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)))

end;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)))end;

hence
x in union (rng (f | (n + 1)))
; :: thesis: verumper cases
( x in union (rng (f | n)) or x in f . n )
by A1, XBOOLE_0:def 3;

end;

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;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

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;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

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;

end;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)end;

hence
x in (union (rng (f | n))) \/ (f . n)
; :: thesis: verumper cases
( X < n or X = n )
by A21, XXREAL_0:1;

end;

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;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