let l1, l2 be Element of NAT ; :: thesis: ( goto l1 = goto l2 implies l1 = l2 )
assume A1: goto l1 = goto l2 ; :: thesis: l1 = l2
A2: goto l1 = SCM-goto l1 by SCMFSA_2:def 16;
A3: goto l2 = SCM-goto l2 by SCMFSA_2:def 16;
( <*l1*> . 1 = l1 & <*l2*> . 1 = l2 ) by FINSEQ_1:57;
hence l1 = l2 by A1, A2, A3, MCART_1:28; :: thesis: verum