let l1, l2 be Nat; :: thesis: ( goto l1 = goto l2 implies l1 = l2 )
assume A1: goto l1 = goto l2 ; :: thesis: l1 = l2
( <*l1*> . 1 = l1 & <*l2*> . 1 = l2 ) by FINSEQ_1:40;
hence l1 = l2 by A1, XTUPLE_0:3; :: thesis: verum