defpred S₁[ Nat] means #Z n is continuous ;

now :: thesis: for r being Real holds (#Z 0) . r = (REAL --> 1) . r

let r be Real; :: thesis: (#Z 0) . r = (REAL --> 1) . r
thus (#Z 0) . r = r #Z 0 by TAYLOR_1:def 1
.= 1 by PREPOWER:34
.= (REAL --> 1) . r by XREAL_0:def 1, FUNCOP_1:7 ; :: thesis: verum

end;

then #Z 0 = REAL --> 1 ;
then A1: S₁[ 0 ] ;
A2: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A3: S₁[n] ; :: thesis: S₁[n + 1]
set Z1 = #Z 1;
for r being Real st r in dom (#Z 1) holds
(#Z 1) . r = r

proof

let r be Real; :: thesis: ( r in dom (#Z 1) implies (#Z 1) . r = r )
(#Z 1) . r = r #Z 1 by TAYLOR_1:def 1;
hence ( r in dom (#Z 1) implies (#Z 1) . r = r ) by PREPOWER:35; :: thesis: verum

end;

then #Z 1 is continuous by FCONT_1:40;
then (#Z 1) (#) (#Z n) is continuous by A3;
hence S₁[n + 1] by Lm4; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A2);
hence #Z n is continuous ; :: thesis: verum