let p, g be Real; :: thesis: for f being one-to-one PartFunc of REAL ,REAL st ( f | ].p,g.[ is increasing or f | ].p,g.[ is decreasing ) & ].p,g.[ c= dom f holds
((f | ].p,g.[) " ) | (f .: ].p,g.[) is continuous
let f be one-to-one PartFunc of REAL ,REAL ; :: thesis: ( ( f | ].p,g.[ is increasing or f | ].p,g.[ is decreasing ) & ].p,g.[ c= dom f implies ((f | ].p,g.[) " ) | (f .: ].p,g.[) is continuous )
assume that
A1: ( f | ].p,g.[ is increasing or f | ].p,g.[ is decreasing ) and
A2: ].p,g.[ c= dom f ; :: thesis: ((f | ].p,g.[) " ) | (f .: ].p,g.[) is continuous

now

per cases ( f | ].p,g.[ is increasing or f | ].p,g.[ is decreasing ) by A1;

suppose A3: f | ].p,g.[ is increasing ; :: thesis: ((f | ].p,g.[) " ) | (f .: ].p,g.[) is continuous

A4: now

let r be Real; :: thesis: ( r in f .: ].p,g.[ implies r in dom ((f | ].p,g.[) " ) )
assume r in f .: ].p,g.[ ; :: thesis: r in dom ((f | ].p,g.[) " )
then consider s being Real such that
A5: ( s in dom f & s in ].p,g.[ ) and
A6: r = f . s by PARTFUN2:78;
s in (dom f) /\ ].p,g.[ by A5, XBOOLE_0:def 4;
then A7: s in dom (f | ].p,g.[) by RELAT_1:90;
then r = (f | ].p,g.[) . s by A6, FUNCT_1:70;
then r in rng (f | ].p,g.[) by A7, FUNCT_1:def 5;
hence r in dom ((f | ].p,g.[) " ) by FUNCT_1:55; :: thesis: verum

end;

A8: ((f | ].p,g.[) " ) .: (f .: ].p,g.[) = ((f | ].p,g.[) " ) .: (rng (f | ].p,g.[)) by RELAT_1:148
.= ((f | ].p,g.[) " ) .: (dom ((f | ].p,g.[) " )) by FUNCT_1:55
.= rng ((f | ].p,g.[) " ) by RELAT_1:146
.= dom (f | ].p,g.[) by FUNCT_1:55
.= (dom f) /\ ].p,g.[ by RELAT_1:90
.= ].p,g.[ by A2, XBOOLE_1:28 ;
((f | ].p,g.[) " ) | (f .: ].p,g.[) is increasing by A3, Th17;
hence ((f | ].p,g.[) " ) | (f .: ].p,g.[) is continuous by A4, A8, Th23, SUBSET_1:7; :: thesis: verum

end;

suppose A9: f | ].p,g.[ is decreasing ; :: thesis: ((f | ].p,g.[) " ) | (f .: ].p,g.[) is continuous

A10: now

let r be Real; :: thesis: ( r in f .: ].p,g.[ implies r in dom ((f | ].p,g.[) " ) )
assume r in f .: ].p,g.[ ; :: thesis: r in dom ((f | ].p,g.[) " )
then consider s being Real such that
A11: ( s in dom f & s in ].p,g.[ ) and
A12: r = f . s by PARTFUN2:78;
s in (dom f) /\ ].p,g.[ by A11, XBOOLE_0:def 4;
then A13: s in dom (f | ].p,g.[) by RELAT_1:90;
then r = (f | ].p,g.[) . s by A12, FUNCT_1:70;
then r in rng (f | ].p,g.[) by A13, FUNCT_1:def 5;
hence r in dom ((f | ].p,g.[) " ) by FUNCT_1:55; :: thesis: verum

end;

A14: ((f | ].p,g.[) " ) .: (f .: ].p,g.[) = ((f | ].p,g.[) " ) .: (rng (f | ].p,g.[)) by RELAT_1:148
.= ((f | ].p,g.[) " ) .: (dom ((f | ].p,g.[) " )) by FUNCT_1:55
.= rng ((f | ].p,g.[) " ) by RELAT_1:146
.= dom (f | ].p,g.[) by FUNCT_1:55
.= (dom f) /\ ].p,g.[ by RELAT_1:90
.= ].p,g.[ by A2, XBOOLE_1:28 ;
((f | ].p,g.[) " ) | (f .: ].p,g.[) is decreasing by A9, Th18;
hence ((f | ].p,g.[) " ) | (f .: ].p,g.[) is continuous by A10, A14, Th23, SUBSET_1:7; :: thesis: verum

end;

end;

end;

hence ((f | ].p,g.[) " ) | (f .: ].p,g.[) is continuous ; :: thesis: verum