let a, m be Nat; :: thesis: for F, G being integer-valued FinSequence holds (a * (F ^ G)) mod m = ((a * F) mod m) ^ ((a * G) mod m)
let F, G be integer-valued FinSequence; :: thesis: (a * (F ^ G)) mod m = ((a * F) mod m) ^ ((a * G) mod m)
set FG = F ^ G;
A4: dom (a * (F ^ G)) = dom (F ^ G) by VALUED_1:def 5;
A5: dom (a * G) = dom G by VALUED_1:def 5;
then A6: dom ((a * G) mod m) = dom G by Def1;
A7: dom (a * F) = dom F by VALUED_1:def 5;
then A8: dom ((a * F) mod m) = dom F by Def1;
A9: for x being object st x in dom (F ^ G) holds
((a * (F ^ G)) mod m) . x = (((a * F) mod m) ^ ((a * G) mod m)) . x

proof

set H = F ^ G;
let x be object ; :: thesis: ( x in dom (F ^ G) implies ((a * (F ^ G)) mod m) . x = (((a * F) mod m) ^ ((a * G) mod m)) . x )
assume A10: x in dom (F ^ G) ; :: thesis: ((a * (F ^ G)) mod m) . x = (((a * F) mod m) ^ ((a * G) mod m)) . x

now :: thesis: ((a * (F ^ G)) mod m) . x = (((a * F) mod m) ^ ((a * G) mod m)) . x

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

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

A12: ((a * (F ^ G)) mod m) . x = ((a * (F ^ G)) . x) mod m by A4, A10, Def1
.= (a * ((F ^ G) . x)) mod m by VALUED_1:6
.= (a * (F . x)) mod m by A11, FINSEQ_1:def 7 ;
(((a * F) mod m) ^ ((a * G) mod m)) . x = ((a * F) mod m) . x by A8, A11, FINSEQ_1:def 7
.= ((a * F) . x) mod m by A7, A11, Def1
.= (a * (F . x)) mod m by VALUED_1:6 ;
hence ((a * (F ^ G)) mod m) . x = (((a * F) mod m) ^ ((a * G) mod m)) . x by A12; :: 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
A13: n in dom G and
A14: x = (len F) + n ;
A15: ((a * (F ^ G)) mod m) . x = ((a * (F ^ G)) . x) mod m by A4, A10, Def1
.= (a * ((F ^ G) . x)) mod m by VALUED_1:6
.= (a * (G . n)) mod m by A13, A14, FINSEQ_1:def 7 ;
len ((a * F) mod m) = len (a * F) by Def2
.= len F by NEWTON:2 ;
then (((a * F) mod m) ^ ((a * G) mod m)) . x = ((a * G) mod m) . n by A6, A13, A14, FINSEQ_1:def 7
.= ((a * G) . n) mod m by A5, A13, 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 A15; :: thesis: verum

end;

end;

end;

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

end;

A16: dom ((a * (F ^ G)) mod m) = dom (a * (F ^ G)) by Def1
.= dom (F ^ G) by VALUED_1:def 5 ;
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 Def2
.= Seg ((len (a * F)) + (len (a * G))) by Def2
.= 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 A16, A9; :: thesis: verum