let g, p be 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 :: thesis: h | [.p,g.] is one-to-one

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 :: thesis: for p1, p2 being Element of REAL st p1 in dom (h | [.p,g.]) & p2 in dom (h | [.p,g.]) & (h | [.p,g.]) . p1 = (h | [.p,g.]) . p2 holds
p1 = p2

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 that
A3: p1 in dom (h | [.p,g.]) and
A4: p2 in dom (h | [.p,g.]) and
A5: (h | [.p,g.]) . p1 = (h | [.p,g.]) . p2 ; :: thesis: p1 = p2
A6: ( p1 in [.p,g.] /\ (dom h) & p2 in [.p,g.] /\ (dom h) ) by A3, A4, RELAT_1:61;
A7: h . p1 = (h | [.p,g.]) . p2 by A3, A5, FUNCT_1:47
.= h . p2 by A4, FUNCT_1:47 ;
thus p1 = p2 :: thesis: verum

proof

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

now :: thesis: contradiction

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

suppose p1 < p2 ; :: thesis: contradiction

hence contradiction by A2, A7, A6, Th20; :: thesis: verum

end;

suppose p2 < p1 ; :: thesis: contradiction

hence contradiction by A2, A7, A6, Th20; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

end;

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

end;

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

now :: thesis: for p1, p2 being Element of REAL st p1 in dom (h | [.p,g.]) & p2 in dom (h | [.p,g.]) & (h | [.p,g.]) . p1 = (h | [.p,g.]) . p2 holds
p1 = p2

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 that
A10: p1 in dom (h | [.p,g.]) and
A11: p2 in dom (h | [.p,g.]) and
A12: (h | [.p,g.]) . p1 = (h | [.p,g.]) . p2 ; :: thesis: p1 = p2
A13: ( p1 in [.p,g.] /\ (dom h) & p2 in [.p,g.] /\ (dom h) ) by A10, A11, RELAT_1:61;
A14: h . p1 = (h | [.p,g.]) . p2 by A10, A12, FUNCT_1:47
.= h . p2 by A11, FUNCT_1:47 ;
thus p1 = p2 :: thesis: verum

proof

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

now :: thesis: contradiction

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

suppose p1 < p2 ; :: thesis: contradiction

hence contradiction by A9, A14, A13, Th21; :: thesis: verum

end;

suppose p2 < p1 ; :: thesis: contradiction

hence contradiction by A9, A14, A13, Th21; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

end;

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

end;

end;

end;

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