let m be CR_Sequence; :: thesis: for j being Nat
for x being Integer st j in dom m holds
(x mod (Product m)) mod (m . j) = x mod (m . j)
let j be Nat; :: thesis: for x being Integer st j in dom m holds
(x mod (Product m)) mod (m . j) = x mod (m . j)
let x be Integer; :: thesis: ( j in dom m implies (x mod (Product m)) mod (m . j) = x mod (m . j) )
assume A1: j in dom m ; :: thesis: (x mod (Product m)) mod (m . j) = x mod (m . j)
consider z being Integer such that
A2: z * (m . j) = Product m by A1, INT_6:10;
(x mod (Product m)) mod (m . j) = (x - ((x div (z * (m . j))) * (z * (m . j)))) mod (m . j) by A2, INT_1:def 10
.= ((x mod (m . j)) - ((0 + (((x div (z * (m . j))) * z) * (m . j))) mod (m . j))) mod (m . j) by INT_6:7
.= ((x mod (m . j)) - (0 mod (m . j))) mod (m . j) by NAT_D:61
.= (x - 0) mod (m . j) by INT_6:7
.= x mod (m . j) ;
hence (x mod (Product m)) mod (m . j) = x mod (m . j) ; :: thesis: verum