let f, f1, f2 be PartFunc of REAL,REAL; :: thesis: ( dom f = (dom f1) \/ (dom f2) & dom f1 is open & dom f2 is open & f1 | (dom f1) is continuous & f2 | (dom f2) is continuous & ( for z being set st z in dom f1 holds
f . z = f1 . z ) & ( for z being set st z in dom f2 holds
f . z = f2 . z ) implies f | (dom f) is continuous )
set X1 = dom f1;
set X2 = dom f2;
assume that
A1: dom f = (dom f1) \/ (dom f2) and
A2: dom f1 is open and
A3: dom f2 is open and
A4: f1 | (dom f1) is continuous and
A5: f2 | (dom f2) is continuous and
A6: for z being set st z in dom f1 holds
f . z = f1 . z and
A7: for z being set st z in dom f2 holds
f . z = f2 . z ; :: thesis: f | (dom f) is continuous
A8: (dom f) /\ (dom f1) = dom f1 by A1, XBOOLE_1:7, XBOOLE_1:28;
A9: dom (f | (dom f2)) = (dom f) /\ (dom f2) by RELAT_1:61;
let x be Real; :: according to FCONT_1:def 2 :: thesis: ( not x in dom (f | (dom f)) or f | (dom f) is_continuous_in x )
assume x in dom (f | (dom f)) ; :: thesis: f | (dom f) is_continuous_in x
then A10: x in dom f ;
A11: (f | ((dom f1) \/ (dom f2))) . x = f . x by A1;
A12: (dom f) /\ (dom f2) = dom f2 by A1, XBOOLE_1:7, XBOOLE_1:28;
A13: dom (f | (dom f1)) = (dom f) /\ (dom f1) by RELAT_1:61;