let a be Int-Location ; :: thesis: for I being Program of SCM+FSA
for k being Element of NAT st k < 6 holds
(card I) + k in dom (while>0 a,I)
let I be Program of SCM+FSA ; :: thesis: for k being Element of NAT st k < 6 holds
(card I) + k in dom (while>0 a,I)
let k be Element of NAT ; :: thesis: ( k < 6 implies (card I) + k in dom (while>0 a,I) )
assume k < 6 ; :: thesis: (card I) + k in dom (while>0 a,I)
then A1: (card I) + k < (card I) + 6 by XREAL_1:8;
card (while>0 a,I) = (card I) + 6 by Th5;
hence (card I) + k in dom (while>0 a,I) by A1, AFINSQ_1:70; :: thesis: verum