let n be Nat; :: thesis: (n !) * ((Partial_Sums eseq) . n) is integer
defpred S₁[ Nat] means ( $1 <= n implies (n !) * ((Partial_Sums eseq) . $1) is integer );

now :: thesis: for k being Nat st ( k <= n implies (n !) * ((Partial_Sums eseq) . k) is integer ) & k + 1 <= n holds
(n !) * ((Partial_Sums eseq) . (k + 1)) is integer

let k be Nat; :: thesis: ( ( k <= n implies (n !) * ((Partial_Sums eseq) . k) is integer ) & k + 1 <= n implies (n !) * ((Partial_Sums eseq) . (k + 1)) is integer )
assume A1: ( k <= n implies (n !) * ((Partial_Sums eseq) . k) is integer ) ; :: thesis: ( k + 1 <= n implies (n !) * ((Partial_Sums eseq) . (k + 1)) is integer )
assume A2: k + 1 <= n ; :: thesis: (n !) * ((Partial_Sums eseq) . (k + 1)) is integer
k + 0 <= k + 1 by XREAL_1:6;
then reconsider i = (n !) * ((Partial_Sums eseq) . k) as Integer by A1, A2, XXREAL_0:2;
(n !) * (eseq . (k + 1)) = (n !) / ((k + 1) !) by Th32;
then reconsider j = (n !) * (eseq . (k + 1)) as Integer by A2, Th36;
A3: i + j is Integer ;
(n !) * ((Partial_Sums eseq) . (k + 1)) = (n !) * (((Partial_Sums eseq) . k) + (eseq . (k + 1))) by SERIES_1:def 1
.= ((n !) * ((Partial_Sums eseq) . k)) + ((n !) * (eseq . (k + 1))) ;
hence (n !) * ((Partial_Sums eseq) . (k + 1)) is integer by A3; :: thesis: verum

end;

then A4: for k being Nat st S₁[k] holds
S₁[k + 1] ;

now :: thesis: ( 0 <= n implies (n !) * ((Partial_Sums eseq) . 0) is integer )

assume 0 <= n ; :: thesis: (n !) * ((Partial_Sums eseq) . 0) is integer
(n !) * ((Partial_Sums eseq) . 0) = (n !) * (eseq . 0) by SERIES_1:def 1
.= (n !) / (0 !) by Th32 ;
hence (n !) * ((Partial_Sums eseq) . 0) is integer by Th36; :: thesis: verum

end;

then A5: S₁[ 0 ] ;
for k being Nat holds S₁[k] from NAT_1:sch 2(A5, A4);
hence (n !) * ((Partial_Sums eseq) . n) is integer ; :: thesis: verum