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 ) )
A1: ( <*a1,f1*> . 1 = a1 & <*a1,f1*> . 2 = f1 ) ;
A2: ( <*a2,f2*> . 1 = a2 & <*a2,f2*> . 2 = f2 ) ;
assume a1 :=len f1 = a2 :=len f2 ; :: thesis: ( a1 = a2 & f1 = f2 )
hence ( a1 = a2 & f1 = f2 ) by A1, A2, XTUPLE_0:3; :: thesis: verum