let x0 be Real; :: thesis: for I being Function of REAL,() st I = (proj (1,1)) " holds
( I is_differentiable_in x0 & diff (I,x0) = <*1*> )

let I be Function of REAL,(); :: thesis: ( I = (proj (1,1)) " implies ( I is_differentiable_in x0 & diff (I,x0) = <*1*> ) )
assume A1: I = (proj (1,1)) " ; :: thesis: ( I is_differentiable_in x0 & diff (I,x0) = <*1*> )
I . jj = <*jj*> by ;
then reconsider r = <*jj*> as Point of () ;
A2: for x being Real st x in [#] REAL holds
I /. x = (x * r) + (0. ())
proof
let x be Real; :: thesis: ( x in [#] REAL implies I /. x = (x * r) + (0. ()) )
reconsider xx = x as Element of REAL by XREAL_0:def 1;
assume x in [#] REAL ; :: thesis: I /. x = (x * r) + (0. ())
I . jj in REAL 1 by ;
then A3: <*1*> is Element of REAL 1 by ;
I /. xx = <*(x * 1)*> by
.= x * <*1*> by RVSUM_1:47 ;
hence I /. x = x * r by
.= (x * r) + (0. ()) by RLVECT_1:4 ;
:: thesis: verum
end;
A4: [#] REAL c= dom I by FUNCT_2:def 1;
then A5: ( I is_differentiable_on [#] REAL & ( for x being Real st x in [#] REAL holds
(I `| ()) . x = r ) ) by ;
A6: x0 in [#] REAL by XREAL_0:def 1;
hence I is_differentiable_in x0 by ; :: thesis: diff (I,x0) = <*1*>
r = (I `| ()) . x0 by
.= diff (I,x0) by ;
hence diff (I,x0) = <*1*> ; :: thesis: verum