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
A10: dom (f | (dom f1)) = (dom f) /\ (dom f1) by RELAT_1:90;
A11: (dom f) /\ (dom f1) = dom f1 by A1, XBOOLE_1:7, XBOOLE_1:28;
A12: dom (f | (dom f2)) = (dom f) /\ (dom f2) by RELAT_1:90;
A13: (dom f) /\ (dom f2) = dom f2 by A1, XBOOLE_1:7, XBOOLE_1:28;
let x be real number ; :: 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 A14: x in dom f by RELAT_1:86;
A15: (f | ((dom f1) \/ (dom f2))) . x = f . x by A1, A14, FUNCT_1:72;

per cases ( x in dom f1 or x in dom f2 ) by A1, A14, XBOOLE_0:def 3;

suppose A16: x in dom f1 ; :: thesis: f | (dom f) is_continuous_in x

then A17: (f | ((dom f1) \/ (dom f2))) . x = f1 . x by A6, A15
.= (f1 | (dom f1)) . x by A16, FUNCT_1:72 ;
for N1 being Neighbourhood of (f | ((dom f1) \/ (dom f2))) . x ex N being Neighbourhood of x st
for x1 being real number st x1 in dom (f | ((dom f1) \/ (dom f2))) & x1 in N holds
(f | ((dom f1) \/ (dom f2))) . x1 in N1

proof

let N1 be Neighbourhood of (f | ((dom f1) \/ (dom f2))) . x; :: thesis: ex N being Neighbourhood of x st
for x1 being real number st x1 in dom (f | ((dom f1) \/ (dom f2))) & x1 in N holds
(f | ((dom f1) \/ (dom f2))) . x1 in N1
x in dom (f1 | (dom f1)) by A16, RELAT_1:86;
then f1 | (dom f1) is_continuous_in x by A4, FCONT_1:def 2;
then consider N being Neighbourhood of x such that
A19: for x1 being real number st x1 in dom (f1 | (dom f1)) & x1 in N holds
(f1 | (dom f1)) . x1 in N1 by A17, FCONT_1:4;
consider N2 being Neighbourhood of x such that
A20: N2 c= dom f1 by A2, A16, RCOMP_1:39;
consider N3 being Neighbourhood of x such that
A21: N3 c= N and
A22: N3 c= N2 by RCOMP_1:38;
take N3 ; :: thesis: for x1 being real number st x1 in dom (f | ((dom f1) \/ (dom f2))) & x1 in N3 holds
(f | ((dom f1) \/ (dom f2))) . x1 in N1
let x1 be real number ; :: thesis: ( x1 in dom (f | ((dom f1) \/ (dom f2))) & x1 in N3 implies (f | ((dom f1) \/ (dom f2))) . x1 in N1 )
assume that
A23: x1 in dom (f | ((dom f1) \/ (dom f2))) and
A24: x1 in N3 ; :: thesis: (f | ((dom f1) \/ (dom f2))) . x1 in N1

per cases ( x1 in dom (f | (dom f1)) or not x1 in dom (f | (dom f1)) ) ;

suppose A25: x1 in dom (f | (dom f1)) ; :: thesis: (f | ((dom f1) \/ (dom f2))) . x1 in N1

then A26: x1 in dom f1 by A10, XBOOLE_0:def 4;
A27: dom (f | (dom f1)) = (dom f1) /\ (dom f1) by A1, A10, XBOOLE_1:7, XBOOLE_1:28
.= dom (f1 | (dom f1)) by RELAT_1:90 ;
(f | ((dom f1) \/ (dom f2))) . x1 = f . x1 by A23, FUNCT_1:70
.= f1 . x1 by A6, A26
.= (f1 | (dom f1)) . x1 by A26, FUNCT_1:72 ;
hence (f | ((dom f1) \/ (dom f2))) . x1 in N1 by A19, A21, A24, A25, A27; :: thesis: verum

end;

suppose A28: not x1 in dom (f | (dom f1)) ; :: thesis: (f | ((dom f1) \/ (dom f2))) . x1 in N1

x1 in N2 by A22, A24;
hence (f | ((dom f1) \/ (dom f2))) . x1 in N1 by A10, A11, A20, A28; :: thesis: verum

end;

end;

end;

hence f | (dom f) is_continuous_in x by A1, FCONT_1:4; :: thesis: verum

end;

suppose A29: x in dom f2 ; :: thesis: f | (dom f) is_continuous_in x

then A30: (f | ((dom f1) \/ (dom f2))) . x = f2 . x by A7, A15
.= (f2 | (dom f2)) . x by A29, FUNCT_1:72 ;
for N1 being Neighbourhood of (f | ((dom f1) \/ (dom f2))) . x ex N being Neighbourhood of x st
for x1 being real number st x1 in dom (f | ((dom f1) \/ (dom f2))) & x1 in N holds
(f | ((dom f1) \/ (dom f2))) . x1 in N1

proof

let N1 be Neighbourhood of (f | ((dom f1) \/ (dom f2))) . x; :: thesis: ex N being Neighbourhood of x st
for x1 being real number st x1 in dom (f | ((dom f1) \/ (dom f2))) & x1 in N holds
(f | ((dom f1) \/ (dom f2))) . x1 in N1
x in dom (f2 | (dom f2)) by A29, RELAT_1:86;
then f2 | (dom f2) is_continuous_in x by A5, FCONT_1:def 2;
then consider N being Neighbourhood of x such that
A32: for x1 being real number st x1 in dom (f2 | (dom f2)) & x1 in N holds
(f2 | (dom f2)) . x1 in N1 by A30, FCONT_1:4;
consider N2 being Neighbourhood of x such that
A33: N2 c= dom f2 by A3, A29, RCOMP_1:39;
consider N3 being Neighbourhood of x such that
A34: N3 c= N and
A35: N3 c= N2 by RCOMP_1:38;
take N3 ; :: thesis: for x1 being real number st x1 in dom (f | ((dom f1) \/ (dom f2))) & x1 in N3 holds
(f | ((dom f1) \/ (dom f2))) . x1 in N1
let x1 be real number ; :: thesis: ( x1 in dom (f | ((dom f1) \/ (dom f2))) & x1 in N3 implies (f | ((dom f1) \/ (dom f2))) . x1 in N1 )
assume that
A36: x1 in dom (f | ((dom f1) \/ (dom f2))) and
A37: x1 in N3 ; :: thesis: (f | ((dom f1) \/ (dom f2))) . x1 in N1

per cases ( x1 in dom (f | (dom f2)) or not x1 in dom (f | (dom f2)) ) ;

suppose A38: x1 in dom (f | (dom f2)) ; :: thesis: (f | ((dom f1) \/ (dom f2))) . x1 in N1

then A39: x1 in dom f2 by A12, XBOOLE_0:def 4;
A40: dom (f | (dom f2)) = (dom f2) /\ (dom f2) by A1, A12, XBOOLE_1:7, XBOOLE_1:28
.= dom (f2 | (dom f2)) by RELAT_1:90 ;
(f | ((dom f1) \/ (dom f2))) . x1 = f . x1 by A36, FUNCT_1:70
.= f2 . x1 by A7, A39
.= (f2 | (dom f2)) . x1 by A39, FUNCT_1:72 ;
hence (f | ((dom f1) \/ (dom f2))) . x1 in N1 by A32, A34, A37, A38, A40; :: thesis: verum

end;

suppose A41: not x1 in dom (f | (dom f2)) ; :: thesis: (f | ((dom f1) \/ (dom f2))) . x1 in N1

x1 in N2 by A35, A37;
hence (f | ((dom f1) \/ (dom f2))) . x1 in N1 by A12, A13, A33, A41; :: thesis: verum

end;

end;

end;

hence f | (dom f) is_continuous_in x by A1, FCONT_1:4; :: thesis: verum

end;

end;