reconsider f2 = REAL --> (In (0,REAL)) as Function of REAL,REAL ;
deffunc H1( Real) -> Element of REAL = In ((- $1),REAL);
let f be PartFunc of REAL,REAL; :: thesis: ( f = compreal implies for p being Real holds
( f is_differentiable_in p & diff (f,p) = - 1 ) )
assume A1: f = compreal ; :: thesis: for p being Real holds
( f is_differentiable_in p & diff (f,p) = - 1 )
let p be Real; :: thesis: ( f is_differentiable_in p & diff (f,p) = - 1 )
consider f1 being Function of REAL,REAL such that
A2: for p being Element of REAL holds f1 . p = H1(p) from FUNCT_2:sch 4();
 A3: dom f2 = REAL by FUNCOP_1:13;
for hy1 being non-zero 0 -convergent Real_Sequence holds
( (hy1 ") (#) (f2 /* hy1) is convergent & lim ((hy1 ") (#) (f2 /* hy1)) = 0 )
proof
let hy1 be non-zero 0 -convergent Real_Sequence; :: thesis: ( (hy1 ") (#) (f2 /* hy1) is convergent & lim ((hy1 ") (#) (f2 /* hy1)) = 0 )
A4: for n being Nat holds ((hy1 ") (#) (f2 /* hy1)) . n = In (0,REAL)
proof
let n be Nat; :: thesis: ((hy1 ") (#) (f2 /* hy1)) . n = In (0,REAL)
A5: rng hy1 c= dom f2 by A3;
A6: n in NAT by ORDINAL1:def 12;
((hy1 ") (#) (f2 /* hy1)) . n = ((hy1 ") . n) * ((f2 /* hy1) . n) by SEQ_1:8
.= ((hy1 . n) ") * ((f2 /* hy1) . n) by VALUED_1:10 ;
then ((hy1 ") (#) (f2 /* hy1)) . n = ((hy1 . n) ") * (f2 . (hy1 . n)) by A6, A5, FUNCT_2:108
.= ((hy1 . n) ") * 0 by FUNCOP_1:7
.= 0 ;
hence ((hy1 ") (#) (f2 /* hy1)) . n = In (0,REAL) ; :: thesis: verum
end;
then A7: (hy1 ") (#) (f2 /* hy1) is constant by VALUED_0:def 18;
for n being Nat holds lim ((hy1 ") (#) (f2 /* hy1)) = 0
proof
let n be Nat; :: thesis: lim ((hy1 ") (#) (f2 /* hy1)) = 0
lim ((hy1 ") (#) (f2 /* hy1)) = ((hy1 ") (#) (f2 /* hy1)) . n by A7, SEQ_4:26
.= 0 by A4 ;
hence lim ((hy1 ") (#) (f2 /* hy1)) = 0 ; :: thesis: verum
end;
hence ( (hy1 ") (#) (f2 /* hy1) is convergent & lim ((hy1 ") (#) (f2 /* hy1)) = 0 ) by A7; :: thesis: verum
end;
then A8: f2 is RestFunc by FDIFF_1:def 2;
A9: ex N being Neighbourhood of p st
( N c= dom compreal & ( for r being Real st r in N holds
(compreal . r) - (compreal . p) = (f1 . (r - p)) + (f2 . (r - p)) ) )
proof
take ].(p - 1),(p + 1).[ ; :: thesis: ( ].(p - 1),(p + 1).[ is Neighbourhood of p & ].(p - 1),(p + 1).[ c= dom compreal & ( for r being Real st r in ].(p - 1),(p + 1).[ holds
(compreal . r) - (compreal . p) = (f1 . (r - p)) + (f2 . (r - p)) ) )
for r being Real st r in ].(p - 1),(p + 1).[ holds
(compreal . r) - (compreal . p) = (f1 . (r - p)) + (f2 . (r - p))
proof
let r be Real; :: thesis: ( r in ].(p - 1),(p + 1).[ implies (compreal . r) - (compreal . p) = (f1 . (r - p)) + (f2 . (r - p)) )
A10: for d being Real holds f2 . d = 0 by XREAL_0:def 1, FUNCOP_1:7;
A11: for p being Real holds f1 . p = - p
proof
let p be Real; :: thesis: f1 . p = - p
p in REAL by XREAL_0:def 1;
then f1 . p = H1(p) by A2;
hence f1 . p = - p ; :: thesis: verum
end;
(compreal . r) - (compreal . p) = ((- 1) * r) - (compreal . p) by Lm10
.= (((- 1) * r) - ((- 1) * p)) + 0 by Lm10
.= (- (r - p)) + (f2 . (r - p)) by A10
.= (f1 . (r - p)) + (f2 . (r - p)) by A11 ;
hence ( r in ].(p - 1),(p + 1).[ implies (compreal . r) - (compreal . p) = (f1 . (r - p)) + (f2 . (r - p)) ) ; :: thesis: verum
end;
hence ( ].(p - 1),(p + 1).[ is Neighbourhood of p & ].(p - 1),(p + 1).[ c= dom compreal & ( for r being Real st r in ].(p - 1),(p + 1).[ holds
(compreal . r) - (compreal . p) = (f1 . (r - p)) + (f2 . (r - p)) ) ) by Lm11, RCOMP_1:def 6; :: thesis: verum
end;
reconsider pp = p as Real ;
A12: 1 in REAL by XREAL_0:def 1;
for p being Real holds f1 . p = (- 1) * p
proof
let p be Real; :: thesis: f1 . p = (- 1) * p
reconsider pp = p as Element of REAL by XREAL_0:def 1;
f1 . p = H1(pp) by A2;
hence f1 . p = (- 1) * p ; :: thesis: verum
end;
then A13: f1 is LinearFunc by FDIFF_1:def 3;
then f is_differentiable_in pp by A1, A8, A9, FDIFF_1:def 4;
then diff (f,pp) = f1 . 1 by A1, A13, A8, A9, FDIFF_1:def 5
.= H1(1) by A2, A12 ;
hence ( f is_differentiable_in p & diff (f,p) = - 1 ) by A1, A13, A8, A9, FDIFF_1:def 4; :: thesis: verum