let a be Int_position; for i being Integer
for n, m being Nat
for I being Program of holds
( m < (card I) + 3 iff m in dom (for-down (a,i,n,I)) )
let i be Integer; for n, m being Nat
for I being Program of holds
( m < (card I) + 3 iff m in dom (for-down (a,i,n,I)) )
let n, m be Nat; for I being Program of holds
( m < (card I) + 3 iff m in dom (for-down (a,i,n,I)) )
let I be Program of ; ( m < (card I) + 3 iff m in dom (for-down (a,i,n,I)) )
card (for-down (a,i,n,I)) = (card I) + 3
by Th39;
hence
( m < (card I) + 3 iff m in dom (for-down (a,i,n,I)) )
by AFINSQ_1:66; verum