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 S1[ 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 S1[k] holds
S1[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 ;
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 ; :: thesis: diff ((#Z 1),x) = 1
thus diff ((#Z 1),x) = ((#Z 1) `| REAL) . x by
.= 1 by ; :: thesis: verum
end;
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A8: S1[k] ; :: thesis: S1[k + 1]
now :: thesis: ( ( k = 0 & S1[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: S1[k + 1]
thus S1[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 ; :: 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)) = () /\ (dom (#Z 1)) by FUNCT_2:def 1
.= () /\ REAL by FUNCT_2:def 1 ;
then #Z (k + 1) = (#Z k) (#) (#Z 1) by ;
hence #Z (k + 1) is_differentiable_in x by ; :: 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
.= (((#Z k) . x) * (diff ((#Z 1),x))) + ((diff ((#Z k),x)) * ((#Z 1) . x)) by
.= (((#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 S1[k + 1] ; :: thesis: verum
end;
A15: S1[ 0 ]
proof
let x be Real; :: thesis: ( #Z 0 is_differentiable_in x & diff ((),x) = 0 * (x #Z (0 - 1)) )
set f = #Z 0;
now :: thesis: for y being object st y in {1} holds
y in rng ()
dom () = REAL by FUNCT_2:def 1;
then consider x being object such that
A16: x in dom () by XBOOLE_0:def 1;
reconsider x1 = x as Real by A16;
let y be object ; :: thesis: ( y in {1} implies y in rng () )
assume A17: y in {1} ; :: thesis: y in rng ()
() . x = x1 #Z 0 by Def1
.= 1 by PREPOWER:34
.= y by ;
hence y in rng () by ; :: thesis: verum
end;
then A18: {1} c= rng () by TARSKI:def 3;
now :: thesis: for y being object st y in rng () holds
y in {1}
let y be object ; :: thesis: ( y in rng () implies y in {1} )
assume y in rng () ; :: thesis: y in {1}
then consider x being object such that
A19: x in dom () and
A20: y = () . x by FUNCT_1:def 3;
reconsider x = x as Real by A19;
() . x = x #Z 0 by Def1
.= 1 by PREPOWER:34 ;
hence y in {1} by ; :: thesis: verum
end;
then rng () c= {1} by TARSKI:def 3;
then A21: rng () = {1} by ;
A22: dom () = [#] REAL by FUNCT_2:def 1;
then A23: #Z 0 is_differentiable_on dom () by ;
A24: x in REAL by XREAL_0:def 1;
then ((#Z 0) `| (dom ())) . x = 0 by ;
hence ( #Z 0 is_differentiable_in x & diff ((),x) = 0 * (x #Z (0 - 1)) ) by ; :: thesis: verum
end;
for n being Nat holds S1[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