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)) /\ (((((multiples p) \/ (multiples q)) \/ (multiples r)) \/ (multiples s)) \/ (multiples t))) = card ((seq ((n + d),k)) /\ (((((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)) /\ (((((multiples p) \/ (multiples q)) \/ (multiples r)) \/ (multiples s)) \/ (multiples t))) = card ((seq ((n + d),k)) /\ (((((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)) /\ (((((multiples p) \/ (multiples q)) \/ (multiples r)) \/ (multiples s)) \/ (multiples t))) = card ((seq ((n + d),k)) /\ (((((multiples p) \/ (multiples q)) \/ (multiples r)) \/ (multiples s)) \/ (multiples t)))
set S = seq (n,k);
set Sd = seq ((n + d),k);
set Mp = multiples p;
set Mq = multiples q;
set Mr = multiples r;
set Ms = multiples s;
set Mt = multiples t;
set M = ((((multiples p) \/ (multiples q)) \/ (multiples r)) \/ (multiples s)) \/ (multiples t);
reconsider D = d as Element of NAT by ORDINAL1:def 12;
deffunc H₁( Element of NAT ) -> Element of omega = $1 + D;
consider f being Function of NAT,NAT such that
A2: for x being Element of NAT holds f . x = H₁(x) from FUNCT_2:sch 4();
A3: dom f = NAT by FUNCT_2:def 1;
A4: f .: ((seq (n,k)) /\ (((((multiples p) \/ (multiples q)) \/ (multiples r)) \/ (multiples s)) \/ (multiples t))) c= (seq ((n + d),k)) /\ (((((multiples p) \/ (multiples q)) \/ (multiples r)) \/ (multiples s)) \/ (multiples t))

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in f .: ((seq (n,k)) /\ (((((multiples p) \/ (multiples q)) \/ (multiples r)) \/ (multiples s)) \/ (multiples t))) or y in (seq ((n + d),k)) /\ (((((multiples p) \/ (multiples q)) \/ (multiples r)) \/ (multiples s)) \/ (multiples t)) )
assume y in f .: ((seq (n,k)) /\ (((((multiples p) \/ (multiples q)) \/ (multiples r)) \/ (multiples s)) \/ (multiples t))) ; :: thesis: y in (seq ((n + d),k)) /\ (((((multiples p) \/ (multiples q)) \/ (multiples r)) \/ (multiples s)) \/ (multiples t))
then consider x being object such that
A5: ( x in dom f & x in (seq (n,k)) /\ (((((multiples p) \/ (multiples q)) \/ (multiples r)) \/ (multiples s)) \/ (multiples t)) & y = f . x ) by FUNCT_1:def 6;
reconsider x = x as Element of NAT by A5;
( x in (((multiples p) \/ (multiples q)) \/ (multiples r)) \/ (multiples s) or x in multiples t ) by A5, XBOOLE_0:def 3;
then ( x in ((multiples p) \/ (multiples q)) \/ (multiples r) or x in multiples s or x in multiples t ) by XBOOLE_0:def 3;
then ( x in (multiples p) \/ (multiples q) or x in multiples r or x in multiples s or x in multiples t ) by XBOOLE_0:def 3;
then ( x in multiples p or x in multiples q or x in multiples r or x in multiples s or x in multiples t ) by XBOOLE_0:def 3;
then ( x + D in multiples p or x + D in multiples q or x + D in multiples r or x + D in multiples s or x + D in multiples t ) by A1, Th86;
then ( x + D in (multiples p) \/ (multiples q) or x + D in multiples r or x + D in multiples s or x + D in multiples t ) by XBOOLE_0:def 3;
then ( x + D in ((multiples p) \/ (multiples q)) \/ (multiples r) or x + D in multiples s or x + D in multiples t ) by XBOOLE_0:def 3;
then ( x + D in (((multiples p) \/ (multiples q)) \/ (multiples r)) \/ (multiples s) or x + D in multiples t ) by XBOOLE_0:def 3;
then ( x + D in ((((multiples p) \/ (multiples q)) \/ (multiples r)) \/ (multiples s)) \/ (multiples t) & x + D in seq ((n + d),k) ) by XBOOLE_0:def 3, A5, Th87;
then x + D in (((((multiples p) \/ (multiples q)) \/ (multiples r)) \/ (multiples s)) \/ (multiples t)) /\ (seq ((n + d),k)) by XBOOLE_0:def 4;
hence y in (seq ((n + d),k)) /\ (((((multiples p) \/ (multiples q)) \/ (multiples r)) \/ (multiples s)) \/ (multiples t)) by A2, A5; :: thesis: verum

end;

(seq ((n + d),k)) /\ (((((multiples p) \/ (multiples q)) \/ (multiples r)) \/ (multiples s)) \/ (multiples t)) c= f .: ((seq (n,k)) /\ (((((multiples p) \/ (multiples q)) \/ (multiples r)) \/ (multiples s)) \/ (multiples t)))

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in (seq ((n + d),k)) /\ (((((multiples p) \/ (multiples q)) \/ (multiples r)) \/ (multiples s)) \/ (multiples t)) or y in f .: ((seq (n,k)) /\ (((((multiples p) \/ (multiples q)) \/ (multiples r)) \/ (multiples s)) \/ (multiples t))) )
assume A6: y in (seq ((n + d),k)) /\ (((((multiples p) \/ (multiples q)) \/ (multiples r)) \/ (multiples s)) \/ (multiples t)) ; :: thesis: y in f .: ((seq (n,k)) /\ (((((multiples p) \/ (multiples q)) \/ (multiples r)) \/ (multiples s)) \/ (multiples t)))
then reconsider y = y as Nat ;
n + d < y by A6, Th73;
then ( d = (n + d) - n & (n + d) - n <= y - 0 ) by XREAL_1:13;
then reconsider yd = y - d as Element of NAT by NAT_1:21;
A7: y = yd + D ;
then A8: f . yd = y by A2;
( y in (((multiples p) \/ (multiples q)) \/ (multiples r)) \/ (multiples s) or y in multiples t ) by A6, XBOOLE_0:def 3;
then ( y in ((multiples p) \/ (multiples q)) \/ (multiples r) or y in multiples s or y in multiples t ) by XBOOLE_0:def 3;
then ( y in (multiples p) \/ (multiples q) or y in multiples r or y in multiples s or y in multiples t ) by XBOOLE_0:def 3;
then ( y in multiples p or y in multiples q or y in multiples r or y in multiples s or y in multiples t ) by XBOOLE_0:def 3;
then ( yd in multiples p or yd in multiples q or yd in multiples r or yd in multiples s or yd in multiples t ) by A7, A1, Th86;
then ( yd in (multiples p) \/ (multiples q) or yd in multiples r or yd in multiples s or yd in multiples t ) by XBOOLE_0:def 3;
then ( yd in ((multiples p) \/ (multiples q)) \/ (multiples r) or yd in multiples s or yd in multiples t ) by XBOOLE_0:def 3;
then ( yd in (((multiples p) \/ (multiples q)) \/ (multiples r)) \/ (multiples s) or yd in multiples t ) by XBOOLE_0:def 3;
then ( yd in ((((multiples p) \/ (multiples q)) \/ (multiples r)) \/ (multiples s)) \/ (multiples t) & yd in seq (n,k) ) by A7, A6, Th87, XBOOLE_0:def 3;
then yd in (((((multiples p) \/ (multiples q)) \/ (multiples r)) \/ (multiples s)) \/ (multiples t)) /\ (seq (n,k)) by XBOOLE_0:def 4;
hence y in f .: ((seq (n,k)) /\ (((((multiples p) \/ (multiples q)) \/ (multiples r)) \/ (multiples s)) \/ (multiples t))) by A8, A3, FUNCT_1:def 6; :: thesis: verum

end;

then A9: (seq ((n + d),k)) /\ (((((multiples p) \/ (multiples q)) \/ (multiples r)) \/ (multiples s)) \/ (multiples t)) = f .: ((seq (n,k)) /\ (((((multiples p) \/ (multiples q)) \/ (multiples r)) \/ (multiples s)) \/ (multiples t))) by A4, XBOOLE_0:def 10;
A10: f is one-to-one

proof

now :: thesis: for x1, x2 being object st x1 in NAT & x2 in NAT & f . x1 = f . x2 holds
x1 = x2

let x1, x2 be object ; :: thesis: ( x1 in NAT & x2 in NAT & f . x1 = f . x2 implies x1 = x2 )
assume A11: ( x1 in NAT & x2 in NAT & f . x1 = f . x2 ) ; :: thesis: x1 = x2
then reconsider n1 = x1, n2 = x2 as Element of NAT ;
( f . x1 = n1 + D & f . x2 = n2 + D ) by A2;
hence x1 = x2 by A11; :: thesis: verum

end;

hence f is one-to-one by A3, FUNCT_1:def 4; :: thesis: verum

end;

(seq (n,k)) /\ (((((multiples p) \/ (multiples q)) \/ (multiples r)) \/ (multiples s)) \/ (multiples t)),f .: ((seq (n,k)) /\ (((((multiples p) \/ (multiples q)) \/ (multiples r)) \/ (multiples s)) \/ (multiples t))) are_equipotent by A10, A3, XBOOLE_1:1, CARD_1:33;
hence card ((seq (n,k)) /\ (((((multiples p) \/ (multiples q)) \/ (multiples r)) \/ (multiples s)) \/ (multiples t))) = card ((seq ((n + d),k)) /\ (((((multiples p) \/ (multiples q)) \/ (multiples r)) \/ (multiples s)) \/ (multiples t))) by A9, CARD_1:5; :: thesis: verum