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: F is FinSequence of REAL by FINSEQ_2:24, NUMBERS:19;
A2: F mod m is FinSequence of REAL by FINSEQ_2:24, NUMBERS:19;
A3: dom (a * F) = Seg (len (a * F)) by FINSEQ_1:def 3
.= Seg (len F) by A1, NEWTON:2
.= dom F by FINSEQ_1:def 3 ;
A4: dom (a * (F mod m)) = Seg (len (a * (F mod m))) by FINSEQ_1:def 3
.= Seg (len (F mod m)) by A2, NEWTON:2
.= Seg (len F) by Def1
.= dom F by FINSEQ_1:def 3 ;
A5: for x being object st x in dom F holds
((a * (F mod m)) mod m) . x = ((a * F) mod m) . x
proof
let x be object ; :: thesis: ( x in dom F implies ((a * (F mod m)) mod m) . x = ((a * F) mod m) . x )
assume A6: 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 A4, A6, Def1
.= (a * ((F mod m) . x)) mod m by RVSUM_1:44
.= (a * ((F . x) mod m)) mod m by A6, Def1
.= (a * (F . x)) mod m by Th7
.= ((a * F) . x) mod m by RVSUM_1:44
.= ((a * F) mod m) . x by A3, A6, Def1 ;
hence ((a * (F mod m)) mod m) . x = ((a * F) mod m) . x ; :: thesis: verum
end;
A7: 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 A1, 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 A2, 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 A7, A5; :: thesis: verum