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_{1}[ 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_{1}[p] holds

S_{1}[p ^ <%l%>]
_{1}[ <%> NAT]
_{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 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

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

S

proof

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

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

let l be Element of NAT ; :: 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 NAT ; :: thesis: ( S

assume A3: S

thus S

proof

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

defpred S_{2}[ 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_{2}[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_{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;

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;defpred S

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

consider p9 being XFinSequence of NAT such that

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 < 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;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

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 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;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

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

proof

for p being XFinSequence of NAT holds S
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

A15: 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 A15;

hence (Sum (<%> NAT)) mod n = (Sum e) mod n by AFINSQ_1:15; :: thesis: verum

end;e . i = ((<%> NAT) . i) mod n ) implies (Sum (<%> NAT)) mod n = (Sum e) mod n )

assume that

A15: 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 A15;

hence (Sum (<%> NAT)) mod n = (Sum e) mod n by AFINSQ_1:15; :: thesis: verum

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