let n be Nat; :: thesis: for x being Real holds
( #Z n is_differentiable_in x & diff ((#Z n),x) = n * (x #Z (n - 1)) )
let x be Real; :: thesis: ( #Z n is_differentiable_in x & diff ((#Z n),x) = n * (x #Z (n - 1)) )
defpred S₁[ Nat] means for x being Real holds
( #Z $1 is_differentiable_in x & diff ((#Z $1),x) = $1 * (x #Z ($1 - 1)) );
A1: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

A2: now :: thesis: for x being Real st x in REAL holds
(#Z 1) . x = (1 * x) + 0

let x be Real; :: thesis: ( x in REAL implies (#Z 1) . x = (1 * x) + 0 )
assume x in REAL ; :: thesis: (#Z 1) . x = (1 * x) + 0
thus (#Z 1) . x = x #Z 1 by Def1
.= (1 * x) + 0 by PREPOWER:35 ; :: thesis: verum

end;

A3: [#] REAL is open Subset of REAL ;
A4: REAL c= dom (#Z 1) by FUNCT_2:def 1;
then A5: #Z 1 is_differentiable_on REAL by A2, A3, FDIFF_1:23;
A6: for x being Real holds
( #Z 1 is_differentiable_in x & diff ((#Z 1),x) = 1 )

proof

let x be Real; :: thesis: ( #Z 1 is_differentiable_in x & diff ((#Z 1),x) = 1 )
A7: x in REAL by XREAL_0:def 1;
hence #Z 1 is_differentiable_in x by A3, A5, FDIFF_1:9; :: thesis: diff ((#Z 1),x) = 1
thus diff ((#Z 1),x) = ((#Z 1) `| REAL) . x by A5, A7, FDIFF_1:def 7
.= 1 by A2, A4, A3, A7, FDIFF_1:23 ; :: thesis: verum

end;

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A8: S₁[k] ; :: thesis: S₁[k + 1]

now :: thesis: ( ( k = 0 & S₁[k + 1] ) or ( k <> 0 & ( for x being Real holds
( #Z (k + 1) is_differentiable_in x & diff ((#Z (k + 1)),x) = (k + 1) * (x #Z ((k + 1) - 1)) ) ) ) )

per cases ( k = 0 or k <> 0 ) ;

case A9: k = 0 ; :: thesis: S₁[k + 1]

thus S₁[k + 1] :: thesis: verum

proof

let x be Real; :: thesis: ( #Z (k + 1) is_differentiable_in x & diff ((#Z (k + 1)),x) = (k + 1) * (x #Z ((k + 1) - 1)) )
thus #Z (k + 1) is_differentiable_in x by A6, A9; :: thesis: diff ((#Z (k + 1)),x) = (k + 1) * (x #Z ((k + 1) - 1))
thus diff ((#Z (k + 1)),x) = 1 by A6, A9
.= (k + 1) * (x #Z ((k + 1) - 1)) by A9, PREPOWER:34 ; :: thesis: verum

end;

end;

case k <> 0 ; :: thesis: for x being Real holds
( #Z (k + 1) is_differentiable_in x & diff ((#Z (k + 1)),x) = (k + 1) * (x #Z ((k + 1) - 1)) )

then 1 <= k by NAT_1:14;
then 1 - 1 <= k - 1 by XREAL_1:13;
then reconsider k1 = k - 1 as Element of NAT by INT_1:3;
let x be Real; :: thesis: ( #Z (k + 1) is_differentiable_in x & diff ((#Z (k + 1)),x) = (k + 1) * (x #Z ((k + 1) - 1)) )
A10: REAL = dom (#Z (k + 1)) by FUNCT_2:def 1;
A11: ( x is Real & #Z k is_differentiable_in x ) by A8;
A12: for x being object st x in dom (#Z (k + 1)) holds
(#Z (k + 1)) . x = ((#Z k) . x) * ((#Z 1) . x)

proof

let x be object ; :: thesis: ( x in dom (#Z (k + 1)) implies (#Z (k + 1)) . x = ((#Z k) . x) * ((#Z 1) . x) )
assume x in dom (#Z (k + 1)) ; :: thesis: (#Z (k + 1)) . x = ((#Z k) . x) * ((#Z 1) . x)
then reconsider x1 = x as Real ;
thus (#Z (k + 1)) . x = x1 #Z (k + 1) by Def1
.= (x1 #Z k) * (x1 #Z 1) by Th1
.= ((#Z k) . x) * (x1 #Z 1) by Def1
.= ((#Z k) . x) * ((#Z 1) . x) by Def1 ; :: thesis: verum

end;

A13: #Z 1 is_differentiable_in x by A6;
A14: (dom (#Z k)) /\ (dom (#Z 1)) = ([#] REAL) /\ (dom (#Z 1)) by FUNCT_2:def 1
.= ([#] REAL) /\ REAL by FUNCT_2:def 1 ;
then #Z (k + 1) = (#Z k) (#) (#Z 1) by A10, A12, VALUED_1:def 4;
hence #Z (k + 1) is_differentiable_in x by A11, A13, FDIFF_1:16; :: thesis: diff ((#Z (k + 1)),x) = (k + 1) * (x #Z ((k + 1) - 1))
thus diff ((#Z (k + 1)),x) = diff (((#Z k) (#) (#Z 1)),x) by A14, A10, A12, VALUED_1:def 4
.= (((#Z k) . x) * (diff ((#Z 1),x))) + ((diff ((#Z k),x)) * ((#Z 1) . x)) by A11, A13, FDIFF_1:16
.= (((#Z k) . x) * 1) + ((diff ((#Z k),x)) * ((#Z 1) . x)) by A6
.= ((x #Z k) * 1) + ((diff ((#Z k),x)) * ((#Z 1) . x)) by Def1
.= ((x #Z k) * 1) + ((diff ((#Z k),x)) * (x #Z 1)) by Def1
.= (x #Z k) + ((k * (x #Z k1)) * (x #Z 1)) by A8
.= (x #Z k) + (k * ((x #Z k1) * (x #Z 1)))
.= (x #Z k) + (k * (x #Z (k1 + 1))) by Th1
.= (k + 1) * (x #Z ((k + 1) - 1)) ; :: thesis: verum

end;

end;

end;

hence S₁[k + 1] ; :: thesis: verum

end;

A15: S₁[ 0 ]

proof

let x be Real; :: thesis: ( #Z 0 is_differentiable_in x & diff ((#Z 0),x) = 0 * (x #Z (0 - 1)) )
set f = #Z 0;

now :: thesis: for y being object st y in {1} holds
y in rng (#Z 0)

dom (#Z 0) = REAL by FUNCT_2:def 1;
then consider x being object such that
A16: x in dom (#Z 0) by XBOOLE_0:def 1;
reconsider x1 = x as Real by A16;
let y be object ; :: thesis: ( y in {1} implies y in rng (#Z 0) )
assume A17: y in {1} ; :: thesis: y in rng (#Z 0)
(#Z 0) . x = x1 #Z 0 by Def1
.= 1 by PREPOWER:34
.= y by A17, TARSKI:def 1 ;
hence y in rng (#Z 0) by A16, FUNCT_1:def 3; :: thesis: verum

end;

then A18: {1} c= rng (#Z 0) by TARSKI:def 3;

now :: thesis: for y being object st y in rng (#Z 0) holds
y in {1}

let y be object ; :: thesis: ( y in rng (#Z 0) implies y in {1} )
assume y in rng (#Z 0) ; :: thesis: y in {1}
then consider x being object such that
A19: x in dom (#Z 0) and
A20: y = (#Z 0) . x by FUNCT_1:def 3;
reconsider x = x as Real by A19;
(#Z 0) . x = x #Z 0 by Def1
.= 1 by PREPOWER:34 ;
hence y in {1} by A20, TARSKI:def 1; :: thesis: verum

end;

then rng (#Z 0) c= {1} by TARSKI:def 3;
then A21: rng (#Z 0) = {1} by A18, XBOOLE_0:def 10;
A22: dom (#Z 0) = [#] REAL by FUNCT_2:def 1;
then A23: #Z 0 is_differentiable_on dom (#Z 0) by A21, FDIFF_1:11;
A24: x in REAL by XREAL_0:def 1;
then ((#Z 0) `| (dom (#Z 0))) . x = 0 by A21, A22, FDIFF_1:11;
hence ( #Z 0 is_differentiable_in x & diff ((#Z 0),x) = 0 * (x #Z (0 - 1)) ) by A24, A23, A22, FDIFF_1:9, FDIFF_1:def 7; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A15, A1);
hence ( #Z n is_differentiable_in x & diff ((#Z n),x) = n * (x #Z (n - 1)) ) ; :: thesis: verum