let a1, a2 be Int-Location ; :: thesis: for f1, f2 being FinSeq-Location st a1 :=len f1 = a2 :=len f2 holds
( a1 = a2 & f1 = f2 )
let f1, f2 be FinSeq-Location ; :: thesis: ( a1 :=len f1 = a2 :=len f2 implies ( a1 = a2 & f1 = f2 ) )
assume A1: a1 :=len f1 = a2 :=len f2 ; :: thesis: ( a1 = a2 & f1 = f2 )
( <*a1,f1*> . 1 = a1 & <*a1,f1*> . 2 = f1 & <*a2,f2*> . 1 = a2 & <*a2,f2*> . 2 = f2 ) by FINSEQ_1:61;
hence ( a1 = a2 & f1 = f2 ) by A1, ZFMISC_1:33; :: thesis: verum