let n, k, d be Nat; :: thesis: 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))))
let p, q, r, s, t be Integer; :: thesis: ( p divides d & q divides d & r divides d & s divides d & t divides d implies 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)))) )
assume A1: ( p divides d & q divides d & r divides d & s divides d & t divides d ) ; :: thesis: 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))))
set M = ((((multiples p) \/ (multiples q)) \/ (multiples r)) \/ (multiples s)) \/ (multiples t);
defpred S₁[ Nat] means $1 * (card ((seq (0,d)) /\ (((((multiples p) \/ (multiples q)) \/ (multiples r)) \/ (multiples s)) \/ (multiples t)))) = card ((seq (n,($1 * d))) /\ (((((multiples p) \/ (multiples q)) \/ (multiples r)) \/ (multiples s)) \/ (multiples t)));
seq (n,(0 * d)) = {} by CALCUL_2:2;
then A2: S₁[ 0 ] ;
A3: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A4: S₁[i] ; :: thesis: S₁[i + 1]
A5: card ((seq ((0 + (n + (i * d))),d)) /\ (((((multiples p) \/ (multiples q)) \/ (multiples r)) \/ (multiples s)) \/ (multiples t))) = card ((seq (0,d)) /\ (((((multiples p) \/ (multiples q)) \/ (multiples r)) \/ (multiples s)) \/ (multiples t))) by A1, Th89;
A6: (seq (n,(i * d))) /\ (((((multiples p) \/ (multiples q)) \/ (multiples r)) \/ (multiples s)) \/ (multiples t)) misses (seq ((n + (i * d)),d)) /\ (((((multiples p) \/ (multiples q)) \/ (multiples r)) \/ (multiples s)) \/ (multiples t)) by Th75, XBOOLE_1:76;
seq (n,((i * d) + d)) = (seq (n,(i * d))) \/ (seq ((n + (i * d)),d)) by Th77;
then (seq (n,((i * d) + d))) /\ (((((multiples p) \/ (multiples q)) \/ (multiples r)) \/ (multiples s)) \/ (multiples t)) = ((seq (n,(i * d))) /\ (((((multiples p) \/ (multiples q)) \/ (multiples r)) \/ (multiples s)) \/ (multiples t))) \/ ((seq ((n + (i * d)),d)) /\ (((((multiples p) \/ (multiples q)) \/ (multiples r)) \/ (multiples s)) \/ (multiples t))) by XBOOLE_1:23;
then card ((seq (n,((i * d) + d))) /\ (((((multiples p) \/ (multiples q)) \/ (multiples r)) \/ (multiples s)) \/ (multiples t))) = (card ((seq (n,(i * d))) /\ (((((multiples p) \/ (multiples q)) \/ (multiples r)) \/ (multiples s)) \/ (multiples t)))) + (card ((seq ((n + (i * d)),d)) /\ (((((multiples p) \/ (multiples q)) \/ (multiples r)) \/ (multiples s)) \/ (multiples t)))) by A6, CARD_2:40;
hence S₁[i + 1] by A4, A5; :: thesis: verum

end;

for i being Nat holds S₁[i] from NAT_1:sch 2(A2, A3);
hence 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)))) ; :: thesis: verum