let m be Nat; :: thesis: for F, G being integer-valued FinSequence holds (F ^ G) mod m = (F mod m) ^ (G mod m)
let F, G be integer-valued FinSequence; :: thesis: (F ^ G) mod m = (F mod m) ^ (G mod m)
A1: dom ((F ^ G) mod m) = dom (F ^ G) by Def1;
A2: dom (G mod m) = dom G by Def1;
A3: dom (F mod m) = dom F by Def1;
A4: for x being object st x in dom (F ^ G) holds
((F ^ G) mod m) . x = ((F mod m) ^ (G mod m)) . x

proof

let x be object ; :: thesis: ( x in dom (F ^ G) implies ((F ^ G) mod m) . x = ((F mod m) ^ (G mod m)) . x )
assume A5: x in dom (F ^ G) ; :: thesis: ((F ^ G) mod m) . x = ((F mod m) ^ (G mod m)) . x
then reconsider x = x as Element of NAT ;

now :: thesis: ((F ^ G) mod m) . x = ((F mod m) ^ (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 A5, FINSEQ_1:25;

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

A7: ((F ^ G) mod m) . x = ((F ^ G) . x) mod m by A5, Def1
.= (F . x) mod m by A6, FINSEQ_1:def 7 ;
((F mod m) ^ (G mod m)) . x = (F mod m) . x by A3, A6, FINSEQ_1:def 7
.= (F . x) mod m by A6, Def1 ;
hence ((F ^ G) mod m) . x = ((F mod m) ^ (G mod m)) . x by A7; :: thesis: verum

end;

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

then consider n being Element of NAT such that
A8: n in dom G and
A9: x = (len F) + n ;
A10: ((F ^ G) mod m) . x = ((F ^ G) . x) mod m by A5, Def1
.= (G . n) mod m by A8, A9, FINSEQ_1:def 7 ;
len (F mod m) = len F by Def2;
then ((F mod m) ^ (G mod m)) . x = (G mod m) . n by A2, A8, A9, FINSEQ_1:def 7
.= (G . n) mod m by A8, Def1 ;
hence ((F ^ G) mod m) . x = ((F mod m) ^ (G mod m)) . x by A10; :: thesis: verum

end;

end;

end;

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

end;

dom ((F mod m) ^ (G mod m)) = Seg (len ((F mod m) ^ (G mod m))) by FINSEQ_1:def 3
.= Seg ((len (F mod m)) + (len (G mod m))) by FINSEQ_1:22
.= Seg ((len F) + (len (G mod m))) by Def2
.= Seg ((len F) + (len G)) by Def2
.= Seg (len (F ^ G)) by FINSEQ_1:22
.= dom (F ^ G) by FINSEQ_1:def 3 ;
hence (F ^ G) mod m = (F mod m) ^ (G mod m) by A1, A4; :: thesis: verum