set L = [#] REAL;
let f be one-to-one PartFunc of REAL,REAL; :: thesis: ( ( f | () is increasing or f | () is decreasing ) & f is total implies (f ") | (rng f) is continuous )
assume that
A1: ( f | () is increasing or f | () is decreasing ) and
A2: f is total ; :: thesis: (f ") | (rng f) is continuous
A3: dom f = [#] REAL by ;
now :: thesis: (f ") | (rng f) is continuous
per cases ( f | () is increasing or f | () is decreasing ) by A1;
suppose A4: f | () is increasing ; :: thesis: (f ") | (rng f) is continuous
A5: now :: thesis: for r being Element of REAL st r in f .: () holds
r in dom ((f | ()) ")
let r be Element of REAL ; :: thesis: ( r in f .: () implies r in dom ((f | ()) ") )
assume r in f .: () ; :: thesis: r in dom ((f | ()) ")
then consider s being Element of REAL such that
A6: s in dom f and
s in [#] REAL and
A7: r = f . s by PARTFUN2:59;
s in (dom f) /\ () by ;
then A8: s in dom (f | ()) by RELAT_1:61;
r = (f | ()) . s by A7;
then r in rng (f | ()) by ;
hence r in dom ((f | ()) ") by FUNCT_1:33; :: thesis: verum
end;
A9: ((f | ()) ") .: (f .: ()) = ((f | ()) ") .: (rng (f | ())) by RELAT_1:115
.= ((f | ()) ") .: (dom ((f | ()) ")) by FUNCT_1:33
.= rng ((f | ()) ") by RELAT_1:113
.= dom (f | ()) by FUNCT_1:33
.= (dom f) /\ () by RELAT_1:61
.= REAL by A3 ;
((f | ()) ") | (f .: ()) is increasing by ;
then ((f | ()) ") | (f .: ()) is continuous by ;
then ((f | ()) ") | (rng f) is continuous by ;
hence (f ") | (rng f) is continuous ; :: thesis: verum
end;
suppose A10: f | () is decreasing ; :: thesis: (f ") | (rng f) is continuous
A11: now :: thesis: for r being Element of REAL st r in f .: () holds
r in dom ((f | ()) ")
let r be Element of REAL ; :: thesis: ( r in f .: () implies r in dom ((f | ()) ") )
assume r in f .: () ; :: thesis: r in dom ((f | ()) ")
then consider s being Element of REAL such that
A12: s in dom f and
s in [#] REAL and
A13: r = f . s by PARTFUN2:59;
s in (dom f) /\ () by ;
then A14: s in dom (f | ()) by RELAT_1:61;
r = (f | ()) . s by A13;
then r in rng (f | ()) by ;
hence r in dom ((f | ()) ") by FUNCT_1:33; :: thesis: verum
end;
A15: ((f | ()) ") .: (f .: ()) = ((f | ()) ") .: (rng (f | ())) by RELAT_1:115
.= ((f | ()) ") .: (dom ((f | ()) ")) by FUNCT_1:33
.= rng ((f | ()) ") by RELAT_1:113
.= dom (f | ()) by FUNCT_1:33
.= (dom f) /\ () by RELAT_1:61
.= REAL by A3 ;
((f | ()) ") | (f .: ()) is decreasing by ;
then ((f | ()) ") | (f .: ()) is continuous by ;
then ((f | ()) ") | (rng f) is continuous by ;
hence (f ") | (rng f) is continuous ; :: thesis: verum
end;
end;
end;
hence (f ") | (rng f) is continuous ; :: thesis: verum