let a be Int-Location ; :: thesis: for I being Program of SCM+FSA
for k being Element of NAT st k < 6 holds
insloc 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
insloc k in dom (while=0 a,I)
let k be Element of NAT ; :: thesis: ( k < 6 implies insloc k in dom (while=0 a,I) )
assume A1: k < 6 ; :: thesis: insloc k in dom (while=0 a,I)
6 <= (card I) + 6 by NAT_1:11;
then A2: k < (card I) + 6 by A1, XXREAL_0:2;
card (while=0 a,I) = (card I) + 6 by Th4;
hence insloc k in dom (while=0 a,I) by A2, SCMFSA6A:15; :: thesis: verum