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:70; :: thesis: verum