reconsider f2 = REAL --> 0 as Function of REAL,REAL ;
deffunc H₁( Real) -> Element of REAL = - $1;
let f be PartFunc of REAL,REAL; :: thesis: ( f = compreal implies for p being real number holds
( f is_differentiable_in p & diff (f,p) = - 1 ) )
assume A1: f = compreal ; :: thesis: for p being real number holds
( f is_differentiable_in p & diff (f,p) = - 1 )
let p be real number ; :: 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 = H₁(p) from FUNCT_2:sch 4();
A3: dom f2 = REAL by FUNCOP_1:13;
for hy1 being convergent_to_0 Real_Sequence holds
( (hy1 ") (#) (f2 /* hy1) is convergent & lim ((hy1 ") (#) (f2 /* hy1)) = 0 )

proof

let hy1 be convergent_to_0 Real_Sequence; :: thesis: ( (hy1 ") (#) (f2 /* hy1) is convergent & lim ((hy1 ") (#) (f2 /* hy1)) = 0 )
A4: for n being Nat holds ((hy1 ") (#) (f2 /* hy1)) . n = 0

proof

let n be Nat; :: thesis: ((hy1 ") (#) (f2 /* hy1)) . n = 0
A5: rng hy1 c= dom f2 by A3;
A6: n in NAT by ORDINAL1:def 12;
then ((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 = 0 ; :: thesis: verum

end;

then A7: (hy1 ") (#) (f2 /* hy1) is constant by VALUED_0:def 18;
for n being Element of NAT holds lim ((hy1 ") (#) (f2 /* hy1)) = 0

proof

let n be Element of 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 REST 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 number st r in ].(p - 1),(p + 1).[ holds
(compreal . r) - (compreal . p) = (f1 . (r - p)) + (f2 . (r - p))

proof

let r be real number ; :: thesis: ( r in ].(p - 1),(p + 1).[ implies (compreal . r) - (compreal . p) = (f1 . (r - p)) + (f2 . (r - p)) )
A10: for d being real number holds f2 . d = 0

proof

let d be real number ; :: thesis: f2 . d = 0
d is Real by XREAL_0:def 1;
hence f2 . d = 0 by FUNCOP_1:7; :: thesis: verum

end;

A11: for p being real number holds f1 . p = - p

proof

let p be real number ; :: thesis: f1 . p = - p
p is Real by XREAL_0:def 1;
hence f1 . p = - p by A2; :: 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;

for p being Real holds f1 . p = (- 1) * p

proof

let p be Real; :: thesis: f1 . p = (- 1) * p
f1 . p = - p by A2;
hence f1 . p = (- 1) * p ; :: thesis: verum

end;

then A12: f1 is LINEAR by FDIFF_1:def 3;
then f is_differentiable_in p by A1, A8, A9, FDIFF_1:def 4;
then diff (f,p) = f1 . 1 by A1, A12, A8, A9, FDIFF_1:def 5
.= - 1 by A2 ;
hence ( f is_differentiable_in p & diff (f,p) = - 1 ) by A1, A12, A8, A9, FDIFF_1:def 4; :: thesis: verum