let i, j be Element of NAT ; :: thesis: ( 0 <= j & j <= 9 implies not value ((Replace ((digits (200,10)),i,j)),10) is prime )
assume A1: ( 0 <= j & j <= 9 ) ; :: thesis: not value ((Replace ((digits (200,10)),i,j)),10) is prime
then A2: not not j = 0 & ... & not j = 9 ;
A3: len (Replace ((digits (200,10)),i,j)) = len (digits (200,10)) by FUNCT_7:30;

A4: now :: thesis: for a being Nat st a in dom (Replace ((digits (200,10)),i,j)) holds
(Replace ((digits (200,10)),i,j)) . a < 10

let a be Nat; :: thesis: ( a in dom (Replace ((digits (200,10)),i,j)) implies (Replace ((digits (200,10)),i,j)) . b₁ < 10 )
assume A5: a in dom (Replace ((digits (200,10)),i,j)) ; :: thesis: (Replace ((digits (200,10)),i,j)) . b₁ < 10

per cases ( a <> i or a = i ) ;

suppose a <> i ; :: thesis: (Replace ((digits (200,10)),i,j)) . b₁ < 10

then (Replace ((digits (200,10)),i,j)) . a = (digits (200,10)) . a by FUNCT_7:32;
hence (Replace ((digits (200,10)),i,j)) . a < 10 by A5, A3, NUMERAL1:def 2; :: thesis: verum

end;

suppose a = i ; :: thesis: (Replace ((digits (200,10)),i,j)) . b₁ < 10

then (Replace ((digits (200,10)),i,j)) . a <= 9 by A1, A3, A5, FUNCT_7:31;
hence (Replace ((digits (200,10)),i,j)) . a < 10 by XXREAL_0:2; :: thesis: verum

end;

end;

end;

per cases ( i in dom (digits (200,10)) or not i in dom (digits (200,10)) ) ;

suppose i in dom (digits (200,10)) ; :: thesis: not value ((Replace ((digits (200,10)),i,j)),10) is prime

then i in 3 by AFINSQ_1:39, NUMBER11:360;

per cases then ( i = 0 or i = 1 or i = 2 ) by CARD_1:51, ENUMSET1:def 1;

suppose A6: i = 0 ; :: thesis: not value ((Replace ((digits (200,10)),i,j)),10) is prime

per cases ( j = 0 or j = 1 or j = 2 or j = 3 or j = 4 or j = 5 or j = 6 or j = 7 or j = 8 or j = 9 ) by A2;

suppose j = 0 ; :: thesis: not value ((Replace ((digits (200,10)),i,j)),10) is prime

then Replace ((digits (200,10)),i,j) = <%0,0,2%> by A6, Th60, NUMBER11:360;
hence not value ((Replace ((digits (200,10)),i,j)),10) is prime by NUMBER11:360, NUMERAL1:def 2, XPRIMES0:200; :: thesis: verum

end;

suppose j = 1 ; :: thesis: not value ((Replace ((digits (200,10)),i,j)),10) is prime

then Replace ((digits (200,10)),i,j) = <%1,0,2%> by A6, Th60, NUMBER11:360;
hence not value ((Replace ((digits (200,10)),i,j)),10) is prime by Th63, NUMERAL1:def 2, XPRIMES0:201; :: thesis: verum

end;

suppose j = 2 ; :: thesis: not value ((Replace ((digits (200,10)),i,j)),10) is prime

then Replace ((digits (200,10)),i,j) = <%2,0,2%> by A6, Th60, NUMBER11:360;
hence not value ((Replace ((digits (200,10)),i,j)),10) is prime by Th64, NUMERAL1:def 2, XPRIMES0:202; :: thesis: verum

end;

suppose j = 3 ; :: thesis: not value ((Replace ((digits (200,10)),i,j)),10) is prime

then Replace ((digits (200,10)),i,j) = <%3,0,2%> by A6, Th60, NUMBER11:360;
hence not value ((Replace ((digits (200,10)),i,j)),10) is prime by Th65, NUMERAL1:def 2, XPRIMES0:203; :: thesis: verum

end;

suppose j = 4 ; :: thesis: not value ((Replace ((digits (200,10)),i,j)),10) is prime

then Replace ((digits (200,10)),i,j) = <%4,0,2%> by A6, Th60, NUMBER11:360;
hence not value ((Replace ((digits (200,10)),i,j)),10) is prime by NUMBER11:239, NUMERAL1:def 2, XPRIMES0:204; :: thesis: verum

end;

suppose j = 5 ; :: thesis: not value ((Replace ((digits (200,10)),i,j)),10) is prime

then Replace ((digits (200,10)),i,j) = <%5,0,2%> by A6, Th60, NUMBER11:360;
hence not value ((Replace ((digits (200,10)),i,j)),10) is prime by Th66, NUMERAL1:def 2, XPRIMES0:205; :: thesis: verum

end;

suppose j = 6 ; :: thesis: not value ((Replace ((digits (200,10)),i,j)),10) is prime

then Replace ((digits (200,10)),i,j) = <%6,0,2%> by A6, Th60, NUMBER11:360;
hence not value ((Replace ((digits (200,10)),i,j)),10) is prime by Th67, NUMERAL1:def 2, XPRIMES0:206; :: thesis: verum

end;

suppose j = 7 ; :: thesis: not value ((Replace ((digits (200,10)),i,j)),10) is prime

then Replace ((digits (200,10)),i,j) = <%7,0,2%> by A6, Th60, NUMBER11:360;
hence not value ((Replace ((digits (200,10)),i,j)),10) is prime by NUMBER11:937, NUMERAL1:def 2, XPRIMES0:207; :: thesis: verum

end;

suppose j = 8 ; :: thesis: not value ((Replace ((digits (200,10)),i,j)),10) is prime

then Replace ((digits (200,10)),i,j) = <%8,0,2%> by A6, Th60, NUMBER11:360;
hence not value ((Replace ((digits (200,10)),i,j)),10) is prime by NUMBER11:127, NUMERAL1:def 2, XPRIMES0:208; :: thesis: verum

end;

suppose j = 9 ; :: thesis: not value ((Replace ((digits (200,10)),i,j)),10) is prime

then Replace ((digits (200,10)),i,j) = <%9,0,2%> by A6, Th60, NUMBER11:360;
hence not value ((Replace ((digits (200,10)),i,j)),10) is prime by NUMBER11:89, NUMERAL1:def 2, XPRIMES0:209; :: thesis: verum

end;

end;

end;

suppose A7: i = 1 ; :: thesis: not value ((Replace ((digits (200,10)),i,j)),10) is prime

then i <> (len (Replace ((digits (200,10)),i,j))) - 1 by A3, NUMBER11:360, AFINSQ_1:39;
then (Replace ((digits (200,10)),i,j)) . ((len (Replace ((digits (200,10)),i,j))) - 1) = (digits (200,10)) . ((len (digits (200,10))) - 1) by A3, FUNCT_7:32
.= (digits (200,10)) . (3 - 1) by NUMBER11:360, AFINSQ_1:39
.= 2 by NUMBER11:360 ;
then A8: digits ((value ((Replace ((digits (200,10)),i,j)),10)),10) = Replace ((digits (200,10)),i,j) by NUMBER11:5, NUMBER11:360, A3, A4;
digits (2,10) = <%2%> by NUMBER11:3;
then ( len (digits (200,10)) = 3 & len (digits (2,10)) = 1 ) by NUMBER11:360, AFINSQ_1:34, AFINSQ_1:39;
then A9: value ((Replace ((digits (200,10)),i,j)),10) > 2 by A3, A8, NUMBER11:12;
(Replace ((digits (200,10)),i,j)) . 0 = (digits (200,10)) . 0 by FUNCT_7:32, A7
.= 0 by NUMBER11:360 ;
then 2 divides value ((Replace ((digits (200,10)),i,j)),10) by A8, INT_2:12, NUMERAL1:8;
hence not value ((Replace ((digits (200,10)),i,j)),10) is prime by A9; :: thesis: verum

end;

suppose A10: i = 2 ; :: thesis: not value ((Replace ((digits (200,10)),i,j)),10) is prime

then i = 3 - 1 ;
then A11: i = (len (Replace ((digits (200,10)),i,j))) - 1 by A3, NUMBER11:360, AFINSQ_1:39;
i in Segm 3 by A10, NAT_1:44;
then A12: i in dom (digits (200,10)) by NUMBER11:360, AFINSQ_1:39;

per cases ( j <> 0 or j = 0 ) ;

suppose j <> 0 ; :: thesis: not value ((Replace ((digits (200,10)),i,j)),10) is prime

then (Replace ((digits (200,10)),i,j)) . ((len (Replace ((digits (200,10)),i,j))) - 1) <> 0 by A11, A12, FUNCT_7:31;
then A13: digits ((value ((Replace ((digits (200,10)),i,j)),10)),10) = Replace ((digits (200,10)),i,j) by NUMBER11:5, NUMBER11:360, A3, A4;
digits (2,10) = <%2%> by NUMBER11:3;
then ( len (digits (200,10)) = 3 & len (digits (2,10)) = 1 ) by NUMBER11:360, AFINSQ_1:34, AFINSQ_1:39;
then A14: value ((Replace ((digits (200,10)),i,j)),10) > 2 by A3, A13, NUMBER11:12;
(Replace ((digits (200,10)),i,j)) . 0 = (digits (200,10)) . 0 by FUNCT_7:32, A10
.= 0 by NUMBER11:360 ;
then 2 divides value ((Replace ((digits (200,10)),i,j)),10) by A13, INT_2:12, NUMERAL1:8;
hence not value ((Replace ((digits (200,10)),i,j)),10) is prime by A14; :: thesis: verum

end;

suppose j = 0 ; :: thesis: not value ((Replace ((digits (200,10)),i,j)),10) is prime

then value ((Replace ((digits (200,10)),i,j)),10) = value (<%0,0,0%>,10) by A10, Th62, NUMBER11:360
.= (value (<%0,0%>,10)) + ((value (<%0%>,10)) * (10 |^ (len <%0,0%>))) by NUMBER16:1
.= (value (<%0,0%>,10)) + (0 * (10 |^ (len <%0,0%>))) by NUMBER11:2
.= (value (<%0%>,10)) + ((value (<%0%>,10)) * (10 |^ (len <%0%>))) by NUMBER16:1
.= (value (<%0%>,10)) + (0 * (10 |^ (len <%0%>))) by NUMBER11:2
.= 0 by NUMBER11:2 ;
hence not value ((Replace ((digits (200,10)),i,j)),10) is prime ; :: thesis: verum

end;

end;

end;

end;

end;

suppose not i in dom (digits (200,10)) ; :: thesis: not value ((Replace ((digits (200,10)),i,j)),10) is prime

then Replace ((digits (200,10)),i,j) = digits (200,10) by FUNCT_7:def 3;
hence not value ((Replace ((digits (200,10)),i,j)),10) is prime by XPRIMES0:200, NUMERAL1:def 2; :: thesis: verum

end;

end;