let a be Int_position; :: thesis: for k1 being Integer
for I being Program of holds 0 in dom (if<0 (a,k1,I))
let k1 be Integer; :: thesis: for I being Program of holds 0 in dom (if<0 (a,k1,I))
let I be Program of ; :: thesis: 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; :: thesis: verum