let d, e be XFinSequence of INT ; :: thesis: for n being Integer 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 Integer; :: 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_{1}[ XFinSequence of INT ] means for e being XFinSequence of INT 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 INT

for l being Element of INT st S_{1}[p] holds

S_{1}[p ^ <%l%>]
_{1}[ <%> INT]
by AFINSQ_1:15;

for p being XFinSequence of INT holds S_{1}[p]
from AFINSQ_2:sch 2(A14, A2);

hence (Sum d) mod n = (Sum e) mod n by A1; :: thesis: verum

e . i = (d . i) mod n ) holds

(Sum d) mod n = (Sum e) mod n

let n be Integer; :: 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

e . i = ($1 . i) mod n ) holds

(Sum $1) mod n = (Sum e) mod n;

A2: for p being XFinSequence of INT

for l being Element of INT st S

S

proof

A14:
S
let p be XFinSequence of INT ; :: thesis: for l being Element of INT st S_{1}[p] holds

S_{1}[p ^ <%l%>]

let l be Element of INT ; :: thesis: ( S_{1}[p] implies S_{1}[p ^ <%l%>] )

assume A3: S_{1}[p]
; :: thesis: S_{1}[p ^ <%l%>]

thus S_{1}[p ^ <%l%>]
:: thesis: verum

end;S

let l be Element of INT ; :: thesis: ( S

assume A3: S

thus S

proof

reconsider dop = dom p as Element of NAT by ORDINAL1:def 12;

defpred S_{2}[ set , Integer] means $2 = (p . $1) mod n;

let e be XFinSequence of INT ; :: 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 INT st S_{2}[k,x]

A7: ( dom p9 = Segm dop & ( for k being Nat st k in Segm dop holds

S_{2}[k,p9 . k] ) )
from STIRL2_1:sch 5(A6);

.= (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;

reconsider lmn = l mod n as Element of INT by INT_1:def 2;

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)) mod n by NAT_D:66

.= (((Sum p9) mod n) + (l mod n)) mod n by A3, A7

.= (((Sum p9) mod n) + ((l mod n) mod n)) mod n by Th14

.= ((Sum p9) + (l mod n)) mod n by NAT_D:66

.= ((Sum p9) + (Sum <%lmn%>)) mod n by AFINSQ_2:53

.= (Sum e) mod n by A13, AFINSQ_2:55 ; :: thesis: verum

end;defpred S

let e be XFinSequence of INT ; :: 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 INT st S

proof

consider p9 being XFinSequence of INT such that
let k be Nat; :: thesis: ( k in Segm dop implies ex x being Element of INT st S_{2}[k,x] )

assume k in Segm dop ; :: thesis: ex x being Element of INT st S_{2}[k,x]

reconsider x = (p . k) mod n as Element of INT by INT_1:def 2;

take x ; :: thesis: S_{2}[k,x]

thus S_{2}[k,x]
; :: thesis: verum

end;assume k in Segm dop ; :: thesis: ex x being Element of INT st S

reconsider x = (p . k) mod n as Element of INT by INT_1:def 2;

take x ; :: thesis: S

thus S

A7: ( dom p9 = Segm dop & ( for k being Nat st k in Segm dop holds

S

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

e . k = p9 . k

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 < Segm (dom p9) by NAT_1:44;

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;assume A9: k in dom p9 ; :: thesis: e . k = p9 . k

then k < Segm (dom p9) by NAT_1:44;

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

A10: now :: thesis: for k being Nat st k in dom <%(l mod n)%> holds

e . ((len p9) + k) = <%(l mod n)%> . k

dom e =
(len p) + (len <%l%>)
by A4, AFINSQ_1:def 3
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 A12: k = 0 by NAT_1:44, 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)%> . k by A12, AFINSQ_1:36 ;

:: thesis: verum

end;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 A12: k = 0 by NAT_1:44, 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)%> . k by A12, AFINSQ_1:36 ;

:: thesis: verum

.= (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;

reconsider lmn = l mod n as Element of INT by INT_1:def 2;

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)) mod n by NAT_D:66

.= (((Sum p9) mod n) + (l mod n)) mod n by A3, A7

.= (((Sum p9) mod n) + ((l mod n) mod n)) mod n by Th14

.= ((Sum p9) + (l mod n)) mod n by NAT_D:66

.= ((Sum p9) + (Sum <%lmn%>)) mod n by AFINSQ_2:53

.= (Sum e) mod n by A13, AFINSQ_2:55 ; :: thesis: verum

for p being XFinSequence of INT holds S

hence (Sum d) mod n = (Sum e) mod n by A1; :: thesis: verum