let A be TopSpace; :: thesis: for B being non empty TopSpace
for f being Function of A,B
for C being TopSpace
for X being Subset of A st f is continuous & C is SubSpace of B holds
for h being Function of (A | X),C st h = f | X holds
h is continuous
let B be non empty TopSpace; :: thesis: for f being Function of A,B
for C being TopSpace
for X being Subset of A st f is continuous & C is SubSpace of B holds
for h being Function of (A | X),C st h = f | X holds
h is continuous
let f be Function of A,B; :: thesis: for C being TopSpace
for X being Subset of A st f is continuous & C is SubSpace of B holds
for h being Function of (A | X),C st h = f | X holds
h is continuous
let C be TopSpace; :: thesis: for X being Subset of A st f is continuous & C is SubSpace of B holds
for h being Function of (A | X),C st h = f | X holds
h is continuous
let X be Subset of A; :: thesis: ( f is continuous & C is SubSpace of B implies for h being Function of (A | X),C st h = f | X holds
h is continuous )
assume that
A1: f is continuous and
A2: C is SubSpace of B ; :: thesis: for h being Function of (A | X),C st h = f | X holds
h is continuous
the carrier of (A | X) = X by PRE_TOPC:8;
then reconsider g = f | X as Function of (A | X),B by FUNCT_2:32;
let h be Function of (A | X),C; :: thesis: ( h = f | X implies h is continuous )
assume A3: h = f | X ; :: thesis: h is continuous
g is continuous by A1, TOPMETR:7;
hence h is continuous by A2, A3, PRE_TOPC:27; :: thesis: verum