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