let l1, l2 be Instruction-Location of SCM+FSA ; :: thesis: ( goto l1 = goto l2 implies l1 = l2 )
assume A1: goto l1 = goto l2 ; :: thesis: l1 = l2
consider L1 being Instruction-Location of SCM such that
A2: ( l1 = L1 & goto l1 = goto L1 ) by SCMFSA_2:def 16;
consider L2 being Instruction-Location of SCM such that
A3: ( l2 = L2 & goto l2 = goto L2 ) by SCMFSA_2:def 16;
( <*L1*> . 1 = L1 & <*L2*> . 1 = L2 ) by FINSEQ_1:57;
hence l1 = l2 by A1, A2, A3, ZFMISC_1:33; :: thesis: verum