set f = (ArProg (199,210)) | 10;
set g = ArProg (199,210);
10 c= NAT ;
then B4: 10 c= dom (ArProg (199,210)) by FUNCT_2:def 1;
B0: dom ((ArProg (199,210)) | 10) = (dom (ArProg (199,210))) /\ 10 by RELAT_1:61
.= 10 by B4, XBOOLE_1:28 ;
WW: {199,409,619,829,1039,1249,1459,1669,1879,2089} c= (rng ((ArProg (199,210)) | 10)) /\ SetPrimes
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {199,409,619,829,1039,1249,1459,1669,1879,2089} or x in (rng ((ArProg (199,210)) | 10)) /\ SetPrimes )
assume HH: x in {199,409,619,829,1039,1249,1459,1669,1879,2089} ; :: thesis: x in (rng ((ArProg (199,210)) | 10)) /\ SetPrimes
then x is Prime by XPRIMES1:199, XPRIMES1:409, XPRIMES1:619, XPRIMES1:829, XPRIMES1:1039, XPRIMES1:1249, XPRIMES1:1459, XPRIMES1:1669, XPRIMES1:1879, XPRIMES1:2089, ENUMSET1:def 8;
then x in SetPrimes by NEWTON:def 6;
hence x in (rng ((ArProg (199,210)) | 10)) /\ SetPrimes by XBOOLE_0:def 4, HH, RngForArProg; :: thesis: verum
end;
WV: {199,409,619,829,1039} misses {1249,1459,1669,1879,2089}
proof
assume {199,409,619,829,1039} meets {1249,1459,1669,1879,2089} ; :: thesis: contradiction
then consider x being object such that
F1: ( x in {199,409,619,829,1039} & x in {1249,1459,1669,1879,2089} ) by XBOOLE_0:3;
( x = 199 or x = 409 or x = 619 or x = 829 or x = 1039 ) by F1, ENUMSET1:def 3;
hence contradiction by F1, ENUMSET1:def 3; :: thesis: verum
end;
WZ: 199,409,619,829,1039 are_mutually_distinct ;
WA: card {199,409,619,829,1039} = 5 by WZ, CARD_2:63;
1249,1459,1669,1879,2089 are_mutually_distinct ;
then WB: card {1249,1459,1669,1879,2089} = 5 by CARD_2:63;
(rng ((ArProg (199,210)) | 10)) /\ SetPrimes c= {199,409,619,829,1039,1249,1459,1669,1879,2089}
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (rng ((ArProg (199,210)) | 10)) /\ SetPrimes or x in {199,409,619,829,1039,1249,1459,1669,1879,2089} )
assume x in (rng ((ArProg (199,210)) | 10)) /\ SetPrimes ; :: thesis: x in {199,409,619,829,1039,1249,1459,1669,1879,2089}
then ( x in rng ((ArProg (199,210)) | 10) & x in SetPrimes ) by XBOOLE_0:def 4;
then consider y being object such that
B1: ( y in dom ((ArProg (199,210)) | 10) & x = ((ArProg (199,210)) | 10) . y ) by FUNCT_1:def 3;
B3: x = (ArProg (199,210)) . y by B0, B1, FUNCT_1:49;
( y = 0 or y = 1 or y = 2 or y = 3 or y = 4 or y = 5 or y = 6 or y = 7 or y = 8 or y = 9 ) by CARD_1:58, B0, B1, ENUMSET1:def 8;
hence x in {199,409,619,829,1039,1249,1459,1669,1879,2089} by ENUMSET1:def 8, B3, Th1990, Th1991, Th1992, Th1993, Th1994, Th1995, Th1996, Th1997, Th1998, Th1999; :: thesis: verum
end;
then (rng ((ArProg (199,210)) | 10)) /\ SetPrimes = {199,409,619,829,1039,1249,1459,1669,1879,2089} by WW, XBOOLE_0:def 10
.= {199,409,619,829,1039} \/ {1249,1459,1669,1879,2089} by SetFor10 ;
then card ((rng ((ArProg (199,210)) | 10)) /\ SetPrimes) = (card {199,409,619,829,1039}) + (card {1249,1459,1669,1879,2089}) by CARD_2:40, WV
.= 10 by WA, WB ;
hence card ((rng ((ArProg (199,210)) | 10)) /\ SetPrimes) = 10 ; :: thesis: verum