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;

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

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

then A15: (f | ((dom f1) \/ (dom f2))) . x = f1 . x by A6, A11
.= (f1 | (dom f1)) . x ;
for N1 being Neighbourhood of (f | ((dom f1) \/ (dom f2))) . x ex N being Neighbourhood of x st
for x1 being Real 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 st x1 in dom (f | ((dom f1) \/ (dom f2))) & x1 in N holds
(f | ((dom f1) \/ (dom f2))) . x1 in N1
consider N2 being Neighbourhood of x such that
A16: N2 c= dom f1 by A2, A14, RCOMP_1:18;
x in dom (f1 | (dom f1)) by A14;
then f1 | (dom f1) is_continuous_in x by A4;
then consider N being Neighbourhood of x such that
A17: for x1 being Real st x1 in dom (f1 | (dom f1)) & x1 in N holds
(f1 | (dom f1)) . x1 in N1 by A15, FCONT_1:4;
consider N3 being Neighbourhood of x such that
A18: N3 c= N and
A19: N3 c= N2 by RCOMP_1:17;
take N3 ; :: thesis: for x1 being Real 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; :: thesis: ( x1 in dom (f | ((dom f1) \/ (dom f2))) & x1 in N3 implies (f | ((dom f1) \/ (dom f2))) . x1 in N1 )
assume that
A20: x1 in dom (f | ((dom f1) \/ (dom f2))) and
A21: 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 A22: x1 in dom (f | (dom f1)) ; :: thesis: (f | ((dom f1) \/ (dom f2))) . x1 in N1

A23: dom (f | (dom f1)) = (dom f1) /\ (dom f1) by A1, A13, XBOOLE_1:7, XBOOLE_1:28
.= dom (f1 | (dom f1)) ;
A24: x1 in dom f1 by A13, A22, XBOOLE_0:def 4;
(f | ((dom f1) \/ (dom f2))) . x1 = f . x1 by A20, FUNCT_1:47
.= f1 . x1 by A6, A24
.= (f1 | (dom f1)) . x1 ;
hence (f | ((dom f1) \/ (dom f2))) . x1 in N1 by A17, A18, A21, A22, A23; :: thesis: verum

end;

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

x1 in N2 by A19, A21;
hence (f | ((dom f1) \/ (dom f2))) . x1 in N1 by A13, A8, A16, A25; :: thesis: verum

end;

end;

end;

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

end;

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

then A27: (f | ((dom f1) \/ (dom f2))) . x = f2 . x by A7, A11
.= (f2 | (dom f2)) . x ;
for N1 being Neighbourhood of (f | ((dom f1) \/ (dom f2))) . x ex N being Neighbourhood of x st
for x1 being Real 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 st x1 in dom (f | ((dom f1) \/ (dom f2))) & x1 in N holds
(f | ((dom f1) \/ (dom f2))) . x1 in N1
consider N2 being Neighbourhood of x such that
A28: N2 c= dom f2 by A3, A26, RCOMP_1:18;
x in dom (f2 | (dom f2)) by A26;
then f2 | (dom f2) is_continuous_in x by A5;
then consider N being Neighbourhood of x such that
A29: for x1 being Real st x1 in dom (f2 | (dom f2)) & x1 in N holds
(f2 | (dom f2)) . x1 in N1 by A27, FCONT_1:4;
consider N3 being Neighbourhood of x such that
A30: N3 c= N and
A31: N3 c= N2 by RCOMP_1:17;
take N3 ; :: thesis: for x1 being Real 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; :: thesis: ( x1 in dom (f | ((dom f1) \/ (dom f2))) & x1 in N3 implies (f | ((dom f1) \/ (dom f2))) . x1 in N1 )
assume that
A32: x1 in dom (f | ((dom f1) \/ (dom f2))) and
A33: 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 A34: x1 in dom (f | (dom f2)) ; :: thesis: (f | ((dom f1) \/ (dom f2))) . x1 in N1

A35: dom (f | (dom f2)) = (dom f2) /\ (dom f2) by A1, A9, XBOOLE_1:7, XBOOLE_1:28
.= dom (f2 | (dom f2)) ;
A36: x1 in dom f2 by A9, A34, XBOOLE_0:def 4;
(f | ((dom f1) \/ (dom f2))) . x1 = f . x1 by A32, FUNCT_1:47
.= f2 . x1 by A7, A36
.= (f2 | (dom f2)) . x1 ;
hence (f | ((dom f1) \/ (dom f2))) . x1 in N1 by A29, A30, A33, A34, A35; :: thesis: verum

end;

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

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

end;

end;

end;

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

end;

end;