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 ;
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 ;
A6: (f | n) . X = f . X by ;
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 ;
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 ;
hence x in union (rng (f | (n + 1))) by ; :: 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 ;
then n in (dom f) /\ (n + 1) by ;
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 ;
hence x in union (rng (f | (n + 1))) by ; :: 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 ;
A18: X in (dom f) /\ (n + 1) by ;
then A19: X in Segm (n + 1) by XBOOLE_0:def 4;
A20: X in dom f by ;
reconsider X = X as Element of NAT by A19;
X < n + 1 by ;
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 ;
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 ;
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 ;
(f | n) . X = f . X by ;
then x in union (rng (f | n)) by ;
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 ;
hence x in (union (rng (f | n))) \/ (f . n) by ; :: thesis: verum
end;
end;
end;
hence x in (union (rng (f | n))) \/ (f . n) ; :: thesis: verum
end;