let il be Element of NAT ; :: thesis: goto il = [6,<*il*>]
ex L being Element of NAT st
( L = il & goto il = SCM-goto L ) by SCMFSA_2:def 16;
hence goto il = [6,<*il*>] ; :: thesis: verum