let a, m be Nat; :: thesis: for F being integer-valued Function holds (a (#) (F mod m)) mod m = (a (#) F) mod m
let F be integer-valued Function; :: thesis: (a (#) (F mod m)) mod m = (a (#) F) mod m
A3: dom (a (#) F) = dom F by VALUED_1:def 5;
dom (a (#) (F mod m)) = dom (F mod m) by VALUED_1:def 5;
then A4: dom (a (#) (F mod m)) = dom F by Def1;
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
A1: (a (#) (F mod m)) . x = a * ((F mod m) . x) by VALUED_1:6;
((a (#) (F mod m)) mod m) . x = ((a (#) (F mod m)) . x) mod m by A4, A6, Def1
.= (a * ((F . x) mod m)) mod m by A6, A1, Def1
.= (a * (F . x)) mod m by Th7
.= ((a (#) F) . x) mod m by VALUED_1:6
.= ((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) = dom F by A3, Def1;
dom ((a (#) (F mod m)) mod m) = dom F by A4, Def1;
hence (a (#) (F mod m)) mod m = (a (#) F) mod m by A7, A5; :: thesis: verum