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 A1: ( f is continuous & h is continuous & rng f c= B & B <> {} & C <> {} ) ; :: thesis: ex g being Function of X,Z st
( g is continuous & g = h * f )
then reconsider V = B as non empty Subset of Y ;
reconsider F = C as non empty Subset of Z by A1;
A2: not Z | F is empty ;
A3: not Y | V is empty ;
A4: the carrier of (Y | B) = [#] (Y | B)
.= B by PRE_TOPC:def 10 ;
the carrier of X = dom f by FUNCT_2:def 1;
then reconsider u = f as Function of X,(Y | B) by A1, A4, FUNCT_2:4;
reconsider G = Z | C as non empty TopSpace by A2;
reconsider H = Y | B as non empty TopSpace by A3;
reconsider k = u as Function of X,H ;
A5: u is continuous by A1, TOPMETR:9;
reconsider j = h as Function of H,G ;
A6: j * k is Function of X,G ;
reconsider w = h * k as Function of X,G ;
the carrier of (Z | C) = [#] (Z | C)
.= C by PRE_TOPC:def 10 ;
then reconsider v = h * u as Function of X,Z by A6, FUNCT_2:9;
v is continuous by A1, A5, PRE_TOPC:56;
hence ex g being Function of X,Z st
( g is continuous & g = h * f ) ; :: thesis: verum