let T1, S1, T2, S2 be non empty TopSpace; :: thesis: for R1 being Refinement of T1,S1
for R2 being Refinement of T2,S2
for f being Function of T1,T2
for g being Function of S1,S2
for h being Function of R1,R2 st h = f & h = g & f is continuous & g is continuous holds
h is continuous
let R1 be Refinement of T1,S1; :: thesis: for R2 being Refinement of T2,S2
for f being Function of T1,T2
for g being Function of S1,S2
for h being Function of R1,R2 st h = f & h = g & f is continuous & g is continuous holds
h is continuous
let R2 be Refinement of T2,S2; :: thesis: for f being Function of T1,T2
for g being Function of S1,S2
for h being Function of R1,R2 st h = f & h = g & f is continuous & g is continuous holds
h is continuous
let f be Function of T1,T2; :: thesis: for g being Function of S1,S2
for h being Function of R1,R2 st h = f & h = g & f is continuous & g is continuous holds
h is continuous
let g be Function of S1,S2; :: thesis: for h being Function of R1,R2 st h = f & h = g & f is continuous & g is continuous holds
h is continuous
let h be Function of R1,R2; :: thesis: ( h = f & h = g & f is continuous & g is continuous implies h is continuous )
assume that
A1: h = f and
A2: h = g ; :: thesis: ( not f is continuous or not g is continuous or h is continuous )
A3: [#] S2 <> {} ;
reconsider K = the topology of T2 \/ the topology of S2 as prebasis of R2 by YELLOW_9:def 6;
A4: [#] T2 <> {} ;
assume A5: f is continuous ; :: thesis: ( not g is continuous or h is continuous )
assume A6: g is continuous ; :: thesis: h is continuous
now :: thesis: for A being Subset of R2 st A in K holds
h " A is open
let A be Subset of R2; :: thesis: ( A in K implies h " b1 is open )
assume A7: A in K ; :: thesis: h " b1 is open
per cases ( A in the topology of T2 or A in the topology of S2 ) by A7, XBOOLE_0:def 3;
suppose A8: A in the topology of T2 ; :: thesis: h " b1 is open
then reconsider A1 = A as Subset of T2 ;
A1 is open by A8;
then f " A1 is open by A4, A5, TOPS_2:43;
hence h " A is open by A1, Th20; :: thesis: verum
end;
suppose A9: A in the topology of S2 ; :: thesis: h " b1 is open
then reconsider A1 = A as Subset of S2 ;
A1 is open by A9;
then A10: g " A1 is open by A3, A6, TOPS_2:43;
R1 is Refinement of S1,T1 by YELLOW_9:55;
hence h " A is open by A10, A2, Th20; :: thesis: verum
end;
end;
end;
hence h is continuous by YELLOW_9:36; :: thesis: verum