let X, Y, Z be non empty TopSpace; :: thesis: for B being Subset of Y
for C being Subset of Z
for f being Function of X,Y
for h being Function of (Y | B),(Z | C) st f is continuous & h is continuous & rng f c= B & B <> {} & C <> {} holds
ex g being Function of X,Z st
( g is continuous & g = h * f )
let B be Subset of Y; :: thesis: for C being Subset of Z
for f being Function of X,Y
for h being Function of (Y | B),(Z | C) st f is continuous & h is continuous & rng f c= B & B <> {} & C <> {} holds
ex g being Function of X,Z st
( g is continuous & g = h * f )
let C be Subset of Z; :: thesis: for f being Function of X,Y
for h being Function of (Y | B),(Z | C) st f is continuous & h is continuous & rng f c= B & B <> {} & C <> {} holds
ex g being Function of X,Z st
( g is continuous & g = h * f )
let f be Function of X,Y; :: thesis: for h being Function of (Y | B),(Z | C) st f is continuous & h is continuous & rng f c= B & B <> {} & C <> {} holds
ex g being Function of X,Z st
( g is continuous & g = h * f )
let h be Function of (Y | B),(Z | C); :: thesis: ( f is continuous & h is continuous & rng f c= B & B <> {} & C <> {} implies ex g being Function of X,Z st
( g is continuous & g = h * f ) )
assume that
A1: f is continuous and
A2: h is continuous and
A3: rng f c= B and
A4: B <> {} and
A5: C <> {} ; :: thesis: ex g being Function of X,Z st
( g is continuous & g = h * f )
A6: the carrier of X = dom f by FUNCT_2:def 1;
the carrier of (Y | B) = [#] (Y | B)
.= B by PRE_TOPC:def 5 ;
then reconsider u = f as Function of X,(Y | B) by A3, A6, FUNCT_2:2;
reconsider V = B as non empty Subset of Y by A4;
not Y | V is empty ;
then reconsider H = Y | B as non empty TopSpace ;
reconsider F = C as non empty Subset of Z by A5;
reconsider k = u as Function of X,H ;
not Z | F is empty ;
then reconsider G = Z | C as non empty TopSpace ;
reconsider j = h as Function of H,G ;
A7: the carrier of (Z | C) = [#] (Z | C)
.= C by PRE_TOPC:def 5 ;
j * k is Function of X,G ;
then reconsider v = h * u as Function of X,Z by A7, FUNCT_2:7;
u is continuous by A1, TOPMETR:6;
then v is continuous by A2, A4, A5, PRE_TOPC:26;
hence ex g being Function of X,Z st
( g is continuous & g = h * f ) ; :: thesis: verum