let a, m be Nat; :: thesis: for F being FinSequence of NAT holds (a * (F mod m)) mod m = (a * F) mod m
let F be FinSequence of NAT ; :: thesis: (a * (F mod m)) mod m = (a * F) mod m
A1: dom (a * F) = Seg (len (a * F)) by FINSEQ_1:def 3
.= Seg (len F) by NEWTON:2
.= dom F by FINSEQ_1:def 3 ;
A2: dom (a * (F mod m)) = Seg (len (a * (F mod m))) by FINSEQ_1:def 3
.= Seg (len (F mod m)) by NEWTON:2
.= Seg (len F) by Def1
.= dom F by FINSEQ_1:def 3 ;
A3: for x being set st x in dom F holds
((a * (F mod m)) mod m) . x = ((a * F) mod m) . x

proof

let x be set ; :: thesis: ( x in dom F implies ((a * (F mod m)) mod m) . x = ((a * F) mod m) . x )
assume A4: x in dom F ; :: thesis: ((a * (F mod m)) mod m) . x = ((a * F) mod m) . x
then reconsider x = x as Element of NAT ;
((a * (F mod m)) mod m) . x = ((a * (F mod m)) . x) mod m by A2, A4, Def1
.= (a * ((F mod m) . x)) mod m by RVSUM_1:44
.= (a * ((F . x) mod m)) mod m by A4, Def1
.= (a * (F . x)) mod m by Th9
.= ((a * F) . x) mod m by RVSUM_1:44
.= ((a * F) mod m) . x by A1, A4, Def1 ;
hence ((a * (F mod m)) mod m) . x = ((a * F) mod m) . x ; :: thesis: verum

end;

A5: dom ((a * F) mod m) = Seg (len ((a * F) mod m)) by FINSEQ_1:def 3
.= Seg (len (a * F)) by Def1
.= Seg (len F) by NEWTON:2
.= dom F by FINSEQ_1:def 3 ;
dom ((a * (F mod m)) mod m) = Seg (len ((a * (F mod m)) mod m)) by FINSEQ_1:def 3
.= Seg (len (a * (F mod m))) by Def1
.= Seg (len (F mod m)) by NEWTON:2
.= Seg (len F) by Def1
.= dom F by FINSEQ_1:def 3 ;
hence (a * (F mod m)) mod m = (a * F) mod m by A5, A3, FUNCT_1:2; :: thesis: verum