let n be Nat; :: thesis:
defpred S₁[ Nat] means for F being FinSequence of NAT st len F = $1 & ( for k being Nat st 1 < k & k <= len F holds
(F . k) mod n = 0 ) holds
(Sum F) mod n = (F . 1) mod n;
A1: S₁[ 0 ]

let F be FinSequence of NAT ; :: thesis:
assume A2: len F = 0 ; :: thesis:
F = {} by A2;
hence ( ex k being Nat st
( 1 < k & k <= len F & not (F . k) mod n = 0 ) or (Sum F) mod n = (F . 1) mod n ) by RVSUM_1:72; :: thesis:

end;

A3: for k being Nat st S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis:
assume A4: S₁[k] ; :: thesis:
set k1 = k + 1;
let F be FinSequence of NAT ; :: thesis:
assume that
A5: len F = k + 1 and
A6: for i being Nat st 1 < i & i <= len F holds
(F . i) mod n = 0 ; :: thesis:

end;

not F is empty by A5;
then len F in dom F by FINSEQ_5:6;
then (F | k) ^ <*(F . (k + 1))*> = F | (k + 1) by A5, FINSEQ_5:10
.= F by A5 ;
then A8: Sum F = (Sum (F | k)) + (F . (k + 1)) by RVSUM_1:74;
A9: k <= k + 1 by NAT_1:11;
A10: len (F | k) = k by A5, NAT_1:11, FINSEQ_1:59;
for i being Nat st 1 < i & i <= len (F | k) holds
((F | k) . i) mod n = 0

let i be Nat; :: thesis:
assume A11: ( 1 < i & i <= len (F | k) ) ; :: thesis:
( (F | k) . i = F . i & i <= len F ) by A10, A11, A5, A9, FINSEQ_3:112, XXREAL_0:2;
hence ((F | k) . i) mod n = 0 by A11, A6; :: thesis:

end;

then ( (Sum F) mod n = 0 & 0 = (F . 1) mod n ) by INT_1:def 10;
hence (Sum F) mod n = (F . 1) mod n ; :: thesis:

end;

A15: ( Sum (F | k) is Nat & Sum F is Nat ) by TARSKI:1;
0 + 1 < k + 1 by A7, XREAL_1:8;
then 0 = ((Sum F) - (Sum (F | k))) mod n by A5, A6, A8;
hence (Sum F) mod n = (F . 1) mod n by A13, A15, A14, INT_4:22; :: thesis:

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A1, A3);
hence for F being FinSequence of NAT st ( for k being Nat st 1 < k & k <= len F holds
(F . k) mod n = 0 ) holds
(Sum F) mod n = (F . 1) mod n ; :: thesis: