let a be Int_position ; :: thesis: for i being Integer
for n being Element of NAT
for I being Program of SCMPDS holds card (stop (for-up (a,i,n,I))) = (card I) + 4
let i be Integer; :: thesis: for n being Element of NAT
for I being Program of SCMPDS holds card (stop (for-up (a,i,n,I))) = (card I) + 4
let n be Element of NAT ; :: thesis: for I being Program of SCMPDS holds card (stop (for-up (a,i,n,I))) = (card I) + 4
let I be Program of SCMPDS; :: thesis: card (stop (for-up (a,i,n,I))) = (card I) + 4
thus card (stop (for-up (a,i,n,I))) = (card (for-up (a,i,n,I))) + 1 by COMPOS_1:55
.= ((card I) + 3) + 1 by Th51
.= (card I) + 4 ; :: thesis: verum