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)
A1: F is FinSequence of REAL by FINSEQ_2:24, NUMBERS:19;
A2: G is FinSequence of REAL by FINSEQ_2:24, NUMBERS:19;
reconsider FG = F ^ G as FinSequence of NAT ;
A3: FG is FinSequence of REAL by FINSEQ_2:24, NUMBERS:19;
A4: dom (a * (F ^ G)) = Seg (len (a * FG)) by FINSEQ_1:def 3
.= Seg (len FG) by A3, NEWTON:2
.= dom (F ^ G) by FINSEQ_1:def 3 ;
A5: dom (a * G) = Seg (len (a * G)) by FINSEQ_1:def 3
.= Seg (len G) by A2, NEWTON:2
.= dom G by FINSEQ_1:def 3 ;
A6: 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 A2, NEWTON:2
.= dom G by FINSEQ_1:def 3 ;
A7: 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 ;
A8: 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 ;
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

reconsider H = F ^ G as FinSequence of NAT ;
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
then reconsider x = x as Element of NAT ;

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 * (H . x)) mod m by RVSUM_1:44
.= (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 RVSUM_1:44 ;
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 * (H . x)) mod m by RVSUM_1:44
.= (a * (G . n)) mod m by A13, A14, FINSEQ_1:def 7 ;
len ((a * F) mod m) = len (a * F) by Def1
.= len F by A1, 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) = Seg (len ((a * FG) mod m)) by FINSEQ_1:def 3
.= Seg (len (a * FG)) by Def1
.= Seg (len FG) by A3, 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 A1, NEWTON:2
.= Seg ((len F) + (len G)) by A2, 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