let d, e be XFinSequence of NAT ; :: thesis: for n being Nat st dom d = dom e & ( for i being Nat st i in dom d holds
e . i = (d . i) mod n ) holds
(Sum d) mod n = (Sum e) mod n
let n be Nat; :: thesis: ( dom d = dom e & ( for i being Nat st i in dom d holds
e . i = (d . i) mod n ) implies (Sum d) mod n = (Sum e) mod n )
assume A1: ( dom d = dom e & ( for i being Nat st i in dom d holds
e . i = (d . i) mod n ) ) ; :: thesis: (Sum d) mod n = (Sum e) mod n
defpred S₁[ XFinSequence of NAT ] means for e being XFinSequence of NAT st dom $1 = dom e & ( for i being Nat st i in dom $1 holds
e . i = ($1 . i) mod n ) holds
(Sum $1) mod n = (Sum e) mod n;
A2: for p being XFinSequence of NAT
for l being Element of NAT st S₁[p] holds
S₁[p ^ <%l%>]

proof

let p be XFinSequence of NAT ; :: thesis: for l being Element of NAT st S₁[p] holds
S₁[p ^ <%l%>]
let l be Element of NAT ; :: thesis: ( S₁[p] implies S₁[p ^ <%l%>] )
assume A3: S₁[p] ; :: thesis: S₁[p ^ <%l%>]
thus S₁[p ^ <%l%>] :: thesis: verum

proof

reconsider dop = dom p as Element of NAT by ORDINAL1:def 13;
defpred S₂[ set , set ] means $2 = (p . $1) mod n;
let e be XFinSequence of NAT ; :: thesis: ( dom (p ^ <%l%>) = dom e & ( for i being Nat st i in dom (p ^ <%l%>) holds
e . i = ((p ^ <%l%>) . i) mod n ) implies (Sum (p ^ <%l%>)) mod n = (Sum e) mod n )
assume that
A4: dom (p ^ <%l%>) = dom e and
A5: for i being Nat st i in dom (p ^ <%l%>) holds
e . i = ((p ^ <%l%>) . i) mod n ; :: thesis: (Sum (p ^ <%l%>)) mod n = (Sum e) mod n
A6: for k being Element of NAT st k in dop holds
ex x being Element of NAT st S₂[k,x] ;
consider p' being XFinSequence of NAT such that
A7: ( dom p' = dop & ( for k being Element of NAT st k in dop holds
S₂[k,p' . k] ) ) from STIRL2_1:sch 6(A6);

A8: now

let k be Element of NAT ; :: thesis: ( k in dom p' implies e . k = p' . k )
assume A9: k in dom p' ; :: thesis: e . k = p' . k
then k < dom p' by NAT_1:45;
then k < (len p) + 1 by A7, NAT_1:13;
then k < (len p) + (len <%l%>) by AFINSQ_1:36;
then k in (len p) + (len <%l%>) by NAT_1:45;
then k in dom (p ^ <%l%>) by AFINSQ_1:def 4;
hence e . k = ((p ^ <%l%>) . k) mod n by A5
.= (p . k) mod n by A7, A9, AFINSQ_1:def 4
.= p' . k by A7, A9 ;
:: thesis: verum

end;

A10: now

let k be Element of NAT ; :: thesis: ( k in dom <%(l mod n)%> implies e . ((len p') + k) = <%(l mod n)%> . k )
assume k in dom <%(l mod n)%> ; :: thesis: e . ((len p') + k) = <%(l mod n)%> . k
then A11: k in 1 by AFINSQ_1:36;
then k < 1 by NAT_1:45;
then A12: k = 0 by NAT_1:14;
k in dom <%l%> by A11, AFINSQ_1:36;
hence e . ((len p') + k) = ((p ^ <%l%>) . (len p)) mod n by A5, A7, A12, AFINSQ_1:26
.= l mod n by AFINSQ_1:40
.= <%(l mod n)%> . k by A12, AFINSQ_1:38 ;
:: thesis: verum

end;

dom e = (len p) + (len <%l%>) by A4, AFINSQ_1:def 4
.= (dom p) + 1 by AFINSQ_1:36
.= (len p') + (len <%(l mod n)%>) by A7, AFINSQ_1:36 ;
then A13: e = p' ^ <%(l mod n)%> by A8, A10, AFINSQ_1:def 4;
A14: for i being Nat st i in dom p holds
p' . i = (p . i) mod n by A7;
thus (Sum (p ^ <%l%>)) mod n = ((Sum p) + (Sum <%l%>)) mod n by Th1
.= ((Sum p) + l) mod n by STIRL2_1:44
.= (((Sum p) mod n) + l) mod n by NAT_D:22
.= (((Sum p) mod n) + (l mod n)) mod n by NAT_D:22
.= (((Sum p') mod n) + (l mod n)) mod n by A3, A7, A14
.= ((Sum p') + (l mod n)) mod n by NAT_D:22
.= ((Sum p') + (Sum <%(l mod n)%>)) mod n by STIRL2_1:44
.= (Sum e) mod n by A13, Th1 ; :: thesis: verum

end;

end;

A15: S₁[ <%> NAT ]

proof

let e be XFinSequence of NAT ; :: thesis: ( dom (<%> NAT ) = dom e & ( for i being Nat st i in dom (<%> NAT ) holds
e . i = ((<%> NAT ) . i) mod n ) implies (Sum (<%> NAT )) mod n = (Sum e) mod n )
assume that
A16: dom (<%> NAT ) = dom e and
for i being Nat st i in dom (<%> NAT ) holds
e . i = ((<%> NAT ) . i) mod n ; :: thesis: (Sum (<%> NAT )) mod n = (Sum e) mod n
len e = 0 by A16;
hence (Sum (<%> NAT )) mod n = (Sum e) mod n by AFINSQ_1:18; :: thesis: verum

end;

for p being XFinSequence of NAT holds S₁[p] from STIRL2_1:sch 5(A15, A2);
hence (Sum d) mod n = (Sum e) mod n by A1; :: thesis: verum