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

proof

let x be set ; :: thesis: ( x in dom F implies ((F mod m) mod m) . x = (F mod m) . x )
assume A3: x in dom F ; :: thesis: ((F mod m) mod m) . x = (F mod m) . x
then reconsider x = x as Element of NAT ;
((F mod m) mod m) . x = ((F mod m) . x) mod m by A1, A3, Def1
.= ((F . x) mod m) mod m by A3, Def1
.= (F . x) mod m by Th7
.= (F mod m) . x by A3, Def1 ;
hence ((F mod m) mod m) . x = (F mod m) . x ; :: thesis: verum

end;

dom ((F mod m) mod m) = Seg (len ((F mod m) mod m)) by FINSEQ_1:def 3
.= Seg (len (F mod m)) by Def1
.= Seg (len F) by Def1
.= dom F by FINSEQ_1:def 3 ;
hence (F mod m) mod m = F mod m by A1, A2, FUNCT_1:2; :: thesis: verum