let a, m be Nat; :: thesis: for F, G being FinSequence of NAT holds (a * (F ^ G)) mod m = ((a * F) mod m) ^ ((a * G) mod m)
let F, G be FinSequence of NAT ; :: thesis: (a * (F ^ G)) mod m = ((a * F) mod m) ^ ((a * G) mod m)
reconsider FG = F ^ G as FinSequence of NAT ;
A1: dom (a * (F ^ G)) = Seg (len (a * FG)) by FINSEQ_1:def 3
.= Seg (len FG) by NEWTON:2
.= dom (F ^ G) by FINSEQ_1:def 3 ;
A2: dom (a * G) = Seg (len (a * G)) by FINSEQ_1:def 3
.= Seg (len G) by NEWTON:2
.= dom G by FINSEQ_1:def 3 ;
A3: dom ((a * G) mod m) = Seg (len ((a * G) mod m)) by FINSEQ_1:def 3
.= Seg (len (a * G)) by Def1
.= Seg (len G) by NEWTON:2
.= dom G by FINSEQ_1:def 3 ;
A4: 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 ;
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 ;
A6: for x being set st x in dom (F ^ G) holds
((a * (F ^ G)) mod m) . x = (((a * F) mod m) ^ ((a * G) mod m)) . x

proof

reconsider H = F ^ G as FinSequence of NAT ;
let x be set ; :: thesis: ( x in dom (F ^ G) implies ((a * (F ^ G)) mod m) . x = (((a * F) mod m) ^ ((a * G) mod m)) . x )
assume A7: x in dom (F ^ G) ; :: thesis: ((a * (F ^ G)) mod m) . x = (((a * F) mod m) ^ ((a * G) mod m)) . x
then reconsider x = x as Element of NAT ;

now

per cases ( x in dom F or ex n being Nat st
( n in dom G & x = (len F) + n ) ) by A7, FINSEQ_1:25;

suppose A8: x in dom F ; :: thesis: ((a * (F ^ G)) mod m) . x = (((a * F) mod m) ^ ((a * G) mod m)) . x

A9: ((a * (F ^ G)) mod m) . x = ((a * (F ^ G)) . x) mod m by A1, A7, Def1
.= (a * (H . x)) mod m by RVSUM_1:44
.= (a * (F . x)) mod m by A8, FINSEQ_1:def 7 ;
(((a * F) mod m) ^ ((a * G) mod m)) . x = ((a * F) mod m) . x by A5, A8, FINSEQ_1:def 7
.= ((a * F) . x) mod m by A4, A8, Def1
.= (a * (F . x)) mod m by RVSUM_1:44 ;
hence ((a * (F ^ G)) mod m) . x = (((a * F) mod m) ^ ((a * G) mod m)) . x by A9; :: thesis: verum

end;

suppose ex n being Nat st
( n in dom G & x = (len F) + n ) ; :: thesis: ((a * (F ^ G)) mod m) . x = (((a * F) mod m) ^ ((a * G) mod m)) . x

then consider n being Element of NAT such that
A10: n in dom G and
A11: x = (len F) + n ;
A12: ((a * (F ^ G)) mod m) . x = ((a * (F ^ G)) . x) mod m by A1, A7, Def1
.= (a * (H . x)) mod m by RVSUM_1:44
.= (a * (G . n)) mod m by A10, A11, FINSEQ_1:def 7 ;
len ((a * F) mod m) = len (a * F) by Def1
.= len F by NEWTON:2 ;
then (((a * F) mod m) ^ ((a * G) mod m)) . x = ((a * G) mod m) . n by A3, A10, A11, FINSEQ_1:def 7
.= ((a * G) . n) mod m by A2, A10, Def1
.= (a * (G . n)) mod m by RVSUM_1:44 ;
hence ((a * (F ^ G)) mod m) . x = (((a * F) mod m) ^ ((a * G) mod m)) . x by A12; :: thesis: verum

end;

end;

end;

hence ((a * (F ^ G)) mod m) . x = (((a * F) mod m) ^ ((a * G) mod m)) . x ; :: thesis: verum

end;

A13: dom ((a * (F ^ G)) mod m) = Seg (len ((a * FG) mod m)) by FINSEQ_1:def 3
.= Seg (len (a * FG)) by Def1
.= Seg (len FG) by NEWTON:2
.= dom (F ^ G) by FINSEQ_1:def 3 ;
dom (((a * F) mod m) ^ ((a * G) mod m)) = Seg (len (((a * F) mod m) ^ ((a * G) mod m))) by FINSEQ_1:def 3
.= Seg ((len ((a * F) mod m)) + (len ((a * G) mod m))) by FINSEQ_1:22
.= Seg ((len (a * F)) + (len ((a * G) mod m))) by Def1
.= Seg ((len (a * F)) + (len (a * G))) by Def1
.= Seg ((len F) + (len (a * G))) by NEWTON:2
.= Seg ((len F) + (len G)) by NEWTON:2
.= Seg (len (F ^ G)) by FINSEQ_1:22
.= dom (F ^ G) by FINSEQ_1:def 3 ;
hence (a * (F ^ G)) mod m = ((a * F) mod m) ^ ((a * G) mod m) by A13, A6, FUNCT_1:2; :: thesis: verum