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 ;
thus rng ((ArProg (199,210)) | 10) c= {199,409,619,829,1039,1249,1459,1669,1879,2089} :: according to XBOOLE_0:def 10 :: thesis: {199,409,619,829,1039,1249,1459,1669,1879,2089} c= rng ((ArProg (199,210)) | 10)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng ((ArProg (199,210)) | 10) or x in {199,409,619,829,1039,1249,1459,1669,1879,2089} )
assume x in rng ((ArProg (199,210)) | 10) ; :: thesis: x in {199,409,619,829,1039,1249,1459,1669,1879,2089}
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;

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) )
assume x in {199,409,619,829,1039,1249,1459,1669,1879,2089} ; :: thesis: x in rng ((ArProg (199,210)) | 10)
then HJ: ( x = (ArProg (199,210)) . 0 or x = (ArProg (199,210)) . 1 or x = (ArProg (199,210)) . 2 or x = (ArProg (199,210)) . 3 or x = (ArProg (199,210)) . 4 or x = (ArProg (199,210)) . 5 or x = (ArProg (199,210)) . 6 or x = (ArProg (199,210)) . 7 or x = (ArProg (199,210)) . 8 or x = (ArProg (199,210)) . 9 ) by Th1990, Th1991, Th1992, Th1993, Th1994, Th1995, Th1996, Th1997, Th1998, Th1999, ENUMSET1:def 8;
x in rng ((ArProg (199,210)) | 10)

proof

J3: ( 0 in dom ((ArProg (199,210)) | 10) & 1 in dom ((ArProg (199,210)) | 10) & 2 in dom ((ArProg (199,210)) | 10) & 3 in dom ((ArProg (199,210)) | 10) & 4 in dom ((ArProg (199,210)) | 10) & 5 in dom ((ArProg (199,210)) | 10) & 6 in dom ((ArProg (199,210)) | 10) & 7 in dom ((ArProg (199,210)) | 10) & 8 in dom ((ArProg (199,210)) | 10) & 9 in dom ((ArProg (199,210)) | 10) ) by CARD_1:58, ENUMSET1:def 8, B0;
then ( ((ArProg (199,210)) | 10) . 0 = (ArProg (199,210)) . 0 & ((ArProg (199,210)) | 10) . 1 = (ArProg (199,210)) . 1 & ((ArProg (199,210)) | 10) . 2 = (ArProg (199,210)) . 2 & ((ArProg (199,210)) | 10) . 3 = (ArProg (199,210)) . 3 & ((ArProg (199,210)) | 10) . 4 = (ArProg (199,210)) . 4 & ((ArProg (199,210)) | 10) . 5 = (ArProg (199,210)) . 5 & ((ArProg (199,210)) | 10) . 6 = (ArProg (199,210)) . 6 & ((ArProg (199,210)) | 10) . 7 = (ArProg (199,210)) . 7 & ((ArProg (199,210)) | 10) . 8 = (ArProg (199,210)) . 8 & ((ArProg (199,210)) | 10) . 9 = (ArProg (199,210)) . 9 ) by FUNCT_1:47;
hence x in rng ((ArProg (199,210)) | 10) by J3, FUNCT_1:3, HJ; :: thesis: verum

end;

hence x in rng ((ArProg (199,210)) | 10) ; :: thesis: verum