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 )
deffunc H₁( Real) -> Element of REAL = - $1;
consider f1 being Function of REAL ,REAL such that
A3: for p being Element of REAL holds f1 . p = H₁(p) from FUNCT_2:sch 4();
A4: f1 is LINEAR

proof

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

proof

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

end;

hence f1 is LINEAR by FDIFF_1:def 4; :: thesis: verum

end;

reconsider f2 = REAL --> 0 as Function of REAL ,REAL ;
A8: dom f2 = REAL by FUNCOP_1:19;
A9: f2 is REST

proof

f2 is REST-like PartFunc of REAL ,REAL

proof

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 )
A11: for n being Nat holds ((hy1 " ) (#) (f2 /* hy1)) . n = 0

proof

let n be Nat; :: thesis: ((hy1 " ) (#) (f2 /* hy1)) . n = 0
X: n in NAT by ORDINAL1:def 13;
then A12: ((hy1 " ) (#) (f2 /* hy1)) . n = ((hy1 " ) . n) * ((f2 /* hy1) . n) by SEQ_1:12
.= ((hy1 . n) " ) * ((f2 /* hy1) . n) by VALUED_1:10 ;
rng hy1 c= dom f2 by A8;
then ((hy1 " ) (#) (f2 /* hy1)) . n = ((hy1 . n) " ) * (f2 . (hy1 . n)) by A12, X, FUNCT_2:185
.= ((hy1 . n) " ) * 0 by FUNCOP_1:13
.= 0 ;
hence ((hy1 " ) (#) (f2 /* hy1)) . n = 0 ; :: thesis: verum

end;

then A13: (hy1 " ) (#) (f2 /* hy1) is V8() 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 A13, SEQ_4:41
.= 0 by A11 ;
hence lim ((hy1 " ) (#) (f2 /* hy1)) = 0 ; :: thesis: verum

end;

hence ( (hy1 " ) (#) (f2 /* hy1) is convergent & lim ((hy1 " ) (#) (f2 /* hy1)) = 0 ) by A13; :: thesis: verum

end;

hence f2 is REST-like PartFunc of REAL ,REAL by FDIFF_1:def 3; :: thesis: verum

end;

hence f2 is REST ; :: thesis: verum

end;

A14: 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

A15: 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)) )
A16: 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 A3; :: thesis: verum

end;

A18: 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:13; :: thesis: verum

end;

(compreal . r) - (compreal . p) = ((- 1) * r) - (compreal . p) by Lm11
.= (((- 1) * r) - ((- 1) * p)) + 0 by Lm11
.= (- (r - p)) + (f2 . (r - p)) by A18
.= (f1 . (r - p)) + (f2 . (r - p)) by A16 ;
hence ( r in ].(p - 1),(p + 1).[ implies (compreal . r) - (compreal . p) = (f1 . (r - p)) + (f2 . (r - p)) ) ; :: thesis: verum

end;

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)) ) )
thus ( ].(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 A15, Lm12, RCOMP_1:def 7; :: thesis: verum

end;

then A19: f is_differentiable_in p by A1, A4, A9, FDIFF_1:def 5;
A20: for p being Element of REAL holds f1 . p = - p by A3;
diff f,p = f1 . 1 by A1, A4, A9, A14, A19, FDIFF_1:def 6
.= - 1 by A20 ;
hence ( f is_differentiable_in p & diff f,p = - 1 ) by A1, A4, A9, A14, FDIFF_1:def 5; :: thesis: verum