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: ( [#] (T1 | A) = A & [#] (T2 | (f .: A)) = f .: A ) by PRE_TOPC:def 10;
dom f = the carrier of T1 by FUNCT_2:def 1;
then ( dom (f | A) = A & rng (f | A) = f .: A ) by RELAT_1:91, RELAT_1:148;
hence f | A is Function of (T1 | A),(T2 | (f .: A)) by A1, FUNCT_2:4; :: thesis: verum