let n be Nat; :: thesis: 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
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 ]

proof

let F be FinSequence of NAT ; :: thesis: ( len F = 0 & ( for k being Nat st 1 < k & k <= len F holds
(F . k) mod n = 0 ) implies (Sum F) mod n = (F . 1) mod n )
assume A2: len F = 0 ; :: thesis: ( 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 )
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 ) ; :: thesis: verum

end;

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

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A4: S₁[k] ; :: thesis: S₁[k + 1]
set k1 = k + 1;
let F be FinSequence of NAT ; :: thesis: ( len F = k + 1 & ( for k being Nat st 1 < k & k <= len F holds
(F . k) mod n = 0 ) implies (Sum F) mod n = (F . 1) mod n )
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: (Sum F) mod n = (F . 1) mod n

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

suppose k = 0 ; :: thesis: (Sum F) mod n = (F . 1) mod n

then F = <*(F . 1)*> by A5, FINSEQ_1:40;
hence (Sum F) mod n = (F . 1) mod n ; :: thesis: verum

end;

suppose A7: k > 0 ; :: thesis: (Sum F) mod n = (F . 1) mod n

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

proof

let i be Nat; :: thesis: ( 1 < i & i <= len (F | k) implies ((F | k) . i) mod n = 0 )
assume A11: ( 1 < i & i <= len (F | k) ) ; :: thesis: ((F | k) . i) mod n = 0
( (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: verum

end;

then A12: (Sum (F | k)) mod n = ((F | k) . 1) mod n by A4, A10;
A13: (F . 1) mod n = (Sum (F | k)) mod n by A7, NAT_1:14, A12, FINSEQ_3:112;

per cases ( n = 0 or n > 0 ) ;

suppose n = 0 ; :: thesis: (Sum F) mod n = (F . 1) mod n

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: verum

end;

suppose A14: n > 0 ; :: thesis: (Sum F) mod n = (F . 1) mod n

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: verum

end;

end;

end;

end;

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: verum