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