let n be natural number ; :: thesis: for x being real number holds
( #Z n is_differentiable_in x & diff (#Z n),x = n * (x #Z (n - 1)) )
let x be real number ; :: thesis: ( #Z n is_differentiable_in x & diff (#Z n),x = n * (x #Z (n - 1)) )
defpred S₁[ natural number ] means for x being real number holds
( #Z $1 is_differentiable_in x & diff (#Z $1),x = $1 * (x #Z ($1 - 1)) );
A1: S₁[ 0 ]

proof

set f = #Z 0 ;
A2: dom (#Z 0 ) = [#] REAL by FUNCT_2:def 1;

now

let y be set ; :: thesis: ( y in {1} implies y in rng (#Z 0 ) )
assume A3: y in {1} ; :: thesis: y in rng (#Z 0 )
dom (#Z 0 ) = REAL by FUNCT_2:def 1;
then consider x being set such that
A4: x in dom (#Z 0 ) ;
reconsider x1 = x as Real by A4;
(#Z 0 ) . x = x1 #Z 0 by Def1
.= 1 by PREPOWER:44
.= y by A3, TARSKI:def 1 ;
hence y in rng (#Z 0 ) by A4, FUNCT_1:def 5; :: thesis: verum

end;

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

now

let y be set ; :: thesis: ( y in rng (#Z 0 ) implies y in {1} )
assume A6: y in rng (#Z 0 ) ; :: thesis: y in {1}
consider x being set such that
A7: x in dom (#Z 0 ) and
A8: y = (#Z 0 ) . x by A6, FUNCT_1:def 5;
reconsider x = x as Real by A7;
(#Z 0 ) . x = x #Z 0 by Def1
.= 1 by PREPOWER:44 ;
hence y in {1} by A8, TARSKI:def 1; :: thesis: verum

end;

then rng (#Z 0 ) c= {1} by TARSKI:def 3;
then A9: rng (#Z 0 ) = {1} by A5, XBOOLE_0:def 10;
let x be real number ; :: thesis: ( #Z 0 is_differentiable_in x & diff (#Z 0 ),x = 0 * (x #Z (0 - 1)) )
A10: x is Real by XREAL_0:def 1;
dom (#Z 0 ) = [#] REAL by FUNCT_2:def 1;
then ( #Z 0 is_differentiable_on dom (#Z 0 ) & ((#Z 0 ) `| (dom (#Z 0 ))) . x = 0 ) by A9, A10, FDIFF_1:19;
hence ( #Z 0 is_differentiable_in x & diff (#Z 0 ),x = 0 * (x #Z (0 - 1)) ) by A2, A10, FDIFF_1:16, FDIFF_1:def 8; :: thesis: verum

end;

A11: for k being natural number st S₁[k] holds
S₁[k + 1]

proof

let k be natural number ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A12: S₁[k] ; :: thesis: S₁[k + 1]
A13: ( REAL c= dom (#Z 1) & [#] REAL is open Subset of REAL & ( for x being Real st x in REAL holds
(#Z 1) . x = (1 * x) + 0 ) )

proof

thus REAL c= dom (#Z 1) by FUNCT_2:def 1; :: thesis: ( [#] REAL is open Subset of REAL & ( for x being Real st x in REAL holds
(#Z 1) . x = (1 * x) + 0 ) )
thus [#] REAL is open Subset of REAL ; :: thesis: for x being Real st x in REAL holds
(#Z 1) . x = (1 * x) + 0

now

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

end;

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

end;

then A14: ( #Z 1 is_differentiable_on REAL & ( for x being Real st x in REAL holds
((#Z 1) `| REAL ) . x = 1 ) ) by FDIFF_1:31;
A15: for x being real number holds
( #Z 1 is_differentiable_in x & diff (#Z 1),x = 1 )

proof

let x be real number ; :: thesis: ( #Z 1 is_differentiable_in x & diff (#Z 1),x = 1 )
A16: x is Real by XREAL_0:def 1;
hence #Z 1 is_differentiable_in x by A13, A14, FDIFF_1:16; :: thesis: diff (#Z 1),x = 1
thus diff (#Z 1),x = ((#Z 1) `| REAL ) . x by A14, A16, FDIFF_1:def 8
.= 1 by A13, A16, FDIFF_1:31 ; :: thesis: verum

end;

now

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

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

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

proof

let x be real number ; :: 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 A15, A17; :: thesis: diff (#Z (k + 1)),x = (k + 1) * (x #Z ((k + 1) - 1))
thus diff (#Z (k + 1)),x = 1 by A15, A17
.= (k + 1) * (x #Z ((k + 1) - 1)) by A17, PREPOWER:44 ; :: thesis: verum

end;

end;

case k <> 0 ; :: thesis: for x being real number 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:15;
then reconsider k1 = k - 1 as Element of NAT by INT_1:16;
A18: (dom (#Z k)) /\ (dom (#Z 1)) = ([#] REAL ) /\ (dom (#Z 1)) by FUNCT_2:def 1
.= ([#] REAL ) /\ REAL by FUNCT_2:def 1 ;
A19: REAL = dom (#Z (k + 1)) by FUNCT_2:def 1;
A20: for x being set st x in dom (#Z (k + 1)) holds
(#Z (k + 1)) . x = ((#Z k) . x) * ((#Z 1) . x)

proof

let x be set ; :: 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;

then A21: #Z (k + 1) = (#Z k) (#) (#Z 1) by A18, A19, VALUED_1:def 4;
let x be real number ; :: thesis: ( #Z (k + 1) is_differentiable_in x & diff (#Z (k + 1)),x = (k + 1) * (x #Z ((k + 1) - 1)) )
A22: x is Real by XREAL_0:def 1;
A23: #Z k is_differentiable_in x by A12;
A24: #Z 1 is_differentiable_in x by A15;
hence #Z (k + 1) is_differentiable_in x by A21, A22, A23, FDIFF_1:24; :: 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 A18, A19, A20, VALUED_1:def 4
.= (((#Z k) . x) * (diff (#Z 1),x)) + ((diff (#Z k),x) * ((#Z 1) . x)) by A22, A23, A24, FDIFF_1:24
.= (((#Z k) . x) * 1) + ((diff (#Z k),x) * ((#Z 1) . x)) by A15
.= ((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 A12
.= (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;

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