let T1, T2 be non empty TopSpace; :: thesis: for f being Function of T1,T2
for A being Subset of T1 holds f | A is Function of (T1 | A),(T2 | (f .: A))
let f be Function of T1,T2; :: thesis: for A being Subset of T1 holds f | A is Function of (T1 | A),(T2 | (f .: A))
let A be Subset of T1; :: thesis: f | A is Function of (T1 | A),(T2 | (f .: A))
A1: rng (f | A) = f .: A by RELAT_1:115;
dom f = the carrier of T1 by FUNCT_2:def 1;
then A2: dom (f | A) = A by RELAT_1:62;
( [#] (T1 | A) = A & [#] (T2 | (f .: A)) = f .: A ) by PRE_TOPC:def 5;
hence f | A is Function of (T1 | A),(T2 | (f .: A)) by A2, A1, FUNCT_2:2; :: thesis: verum