let a be Int-Location ; :: thesis: for il being Element of NAT holds a =0_goto il = [7,<*il,a*>]
let il be Element of NAT ; :: thesis: a =0_goto il = [7,<*il,a*>]
ex A being Data-Location ex L being Element of NAT st
( A = a & L = il & A =0_goto L = a =0_goto il ) by SCMFSA_2:def 17;
hence a =0_goto il = [7,<*il,a*>] ; :: thesis: verum