let p, g be Element of REAL ; :: thesis: for h being PartFunc of REAL ,REAL st ( h | [.p,g.] is increasing or h | [.p,g.] is decreasing ) holds
h | [.p,g.] is one-to-one
let h be PartFunc of REAL ,REAL ; :: thesis: ( ( h | [.p,g.] is increasing or h | [.p,g.] is decreasing ) implies h | [.p,g.] is one-to-one )
assume A1: ( h | [.p,g.] is increasing or h | [.p,g.] is decreasing ) ; :: thesis: h | [.p,g.] is one-to-one

now

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

suppose A2: h | [.p,g.] is increasing ; :: thesis: h | [.p,g.] is one-to-one

now

let p1, p2 be Element of REAL ; :: thesis: ( p1 in dom (h | [.p,g.]) & p2 in dom (h | [.p,g.]) & (h | [.p,g.]) . p1 = (h | [.p,g.]) . p2 implies p1 = p2 )
assume A3: ( p1 in dom (h | [.p,g.]) & p2 in dom (h | [.p,g.]) & (h | [.p,g.]) . p1 = (h | [.p,g.]) . p2 ) ; :: thesis: p1 = p2
then A4: h . p1 = (h | [.p,g.]) . p2 by FUNCT_1:70
.= h . p2 by A3, FUNCT_1:70 ;
A5: ( p1 in [.p,g.] /\ (dom h) & p2 in [.p,g.] /\ (dom h) ) by A3, RELAT_1:90;
thus p1 = p2 :: thesis: verum

proof

assume A6: p1 <> p2 ; :: thesis: contradiction

now

per cases ( p1 < p2 or p2 < p1 ) by A6, XXREAL_0:1;

suppose p1 < p2 ; :: thesis: contradiction

hence contradiction by A2, A4, A5, Def2; :: thesis: verum

end;

suppose p2 < p1 ; :: thesis: contradiction

hence contradiction by A2, A4, A5, Def2; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

end;

hence h | [.p,g.] is one-to-one by PARTFUN1:38; :: thesis: verum

end;

suppose A7: h | [.p,g.] is decreasing ; :: thesis: h | [.p,g.] is one-to-one

now

let p1, p2 be Element of REAL ; :: thesis: ( p1 in dom (h | [.p,g.]) & p2 in dom (h | [.p,g.]) & (h | [.p,g.]) . p1 = (h | [.p,g.]) . p2 implies p1 = p2 )
assume A8: ( p1 in dom (h | [.p,g.]) & p2 in dom (h | [.p,g.]) & (h | [.p,g.]) . p1 = (h | [.p,g.]) . p2 ) ; :: thesis: p1 = p2
then A9: h . p1 = (h | [.p,g.]) . p2 by FUNCT_1:70
.= h . p2 by A8, FUNCT_1:70 ;
A10: ( p1 in [.p,g.] /\ (dom h) & p2 in [.p,g.] /\ (dom h) ) by A8, RELAT_1:90;
thus p1 = p2 :: thesis: verum

proof

assume A11: p1 <> p2 ; :: thesis: contradiction

now

per cases ( p1 < p2 or p2 < p1 ) by A11, XXREAL_0:1;

suppose p1 < p2 ; :: thesis: contradiction

hence contradiction by A7, A9, A10, Def3; :: thesis: verum

end;

suppose p2 < p1 ; :: thesis: contradiction

hence contradiction by A7, A9, A10, Def3; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

end;

hence h | [.p,g.] is one-to-one by PARTFUN1:38; :: thesis: verum

end;

end;

end;

hence h | [.p,g.] is one-to-one ; :: thesis: verum