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 12;
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 Nat st k in Segm dop holds
ex x being Element of NAT st S₂[k,x] ;
consider p9 being XFinSequence of NAT such that
A7: ( dom p9 = Segm dop & ( for k being Nat st k in Segm dop holds
S₂[k,p9 . k] ) ) from STIRL2_1:sch 5(A6);

A8: now :: thesis: for k being Nat st k in dom p9 holds
e . k = p9 . k

let k be Nat; :: thesis: ( k in dom p9 implies e . k = p9 . k )
assume A9: k in dom p9 ; :: thesis: e . k = p9 . k
then k < len p9 by AFINSQ_1:86;
then k < (len p) + 1 by A7, NAT_1:13;
then k < (len p) + (len <%l%>) by AFINSQ_1:33;
then k in Segm ((len p) + (len <%l%>)) by NAT_1:44;
then k in dom (p ^ <%l%>) by AFINSQ_1:def 3;
hence e . k = ((p ^ <%l%>) . k) mod n by A5
.= (p . k) mod n by A7, A9, AFINSQ_1:def 3
.= p9 . k by A7, A9 ;
:: thesis: verum

end;

A10: now :: thesis: for k being Nat st k in dom <%(l mod n)%> holds
e . ((len p9) + k) = <%(l mod n)%> . k

let k be Nat; :: thesis: ( k in dom <%(l mod n)%> implies e . ((len p9) + k) = <%(l mod n)%> . k )
assume k in dom <%(l mod n)%> ; :: thesis: e . ((len p9) + k) = <%(l mod n)%> . k
then A11: k in Segm 1 by AFINSQ_1:33;
then k < 1 by NAT_1:44;
then A12: k = 0 by NAT_1:14;
k in dom <%l%> by A11, AFINSQ_1:33;
hence e . ((len p9) + k) = ((p ^ <%l%>) . (len p)) mod n by A5, A7, A12, AFINSQ_1:23
.= l mod n by AFINSQ_1:36
.= <%(l mod n)%> . k by A12 ;
:: thesis: verum

end;

dom e = (len p) + (len <%l%>) by A4, AFINSQ_1:def 3
.= (dom p) + 1 by AFINSQ_1:33
.= (len p9) + (len <%(l mod n)%>) by A7, AFINSQ_1:33 ;
then A13: e = p9 ^ <%(l mod n)%> by A8, A10, AFINSQ_1:def 3;
thus (Sum (p ^ <%l%>)) mod n = ((Sum p) + (Sum <%l%>)) mod n by AFINSQ_2:55
.= ((Sum p) + l) mod n by AFINSQ_2:53
.= (((Sum p) mod n) + l) mod n by NAT_D:22
.= (((Sum p) mod n) + (l mod n)) mod n by NAT_D:23
.= (((Sum p9) mod n) + (l mod n)) mod n by A3, A7
.= ((Sum p9) + (l mod n)) mod n by NAT_D:22
.= ((Sum p9) + (Sum <%(l mod n)%>)) mod n by AFINSQ_2:53
.= (Sum e) mod n by A13, AFINSQ_2:55 ; :: thesis: verum

end;

end;

A14: S₁[ <%> NAT] by AFINSQ_1:15;
for p being XFinSequence of NAT holds S₁[p] from AFINSQ_2:sch 2(A14, A2);
hence (Sum d) mod n = (Sum e) mod n by A1; :: thesis: verum