theorem Th90: :: NUMBER19:90

for n, k, d being Nat
for p, q, r, s, t being Integer st p divides d & q divides d & r divides d & s divides d & t divides d holds
card ((seq (n,(k * d))) /\ (((((multiples p) \/ (multiples q)) \/ (multiples r)) \/ (multiples s)) \/ (multiples t))) = k * (card ((seq (0,d)) /\ (((((multiples p) \/ (multiples q)) \/ (multiples r)) \/ (multiples s)) \/ (multiples t))))