let a be Int_position; for k1 being Integer
for I being Program of holds 0 in dom (if>0 (a,k1,I))
let k1 be Integer; for I being Program of holds 0 in dom (if>0 (a,k1,I))
let I be Program of ; 0 in dom (if>0 (a,k1,I))
set ci = card (if>0 (a,k1,I));
card (if>0 (a,k1,I)) = (card I) + 1
by Th1;
hence
0 in dom (if>0 (a,k1,I))
by AFINSQ_1:66; verum