let a1, a2, b1, b2 be Int-Location; :: thesis: for f1, f2 being FinSeq-Location st (f1,a1) := b1 = (f2,a2) := b2 holds
( a1 = a2 & b1 = b2 & f1 = f2 )
let f1, f2 be FinSeq-Location ; :: thesis: ( (f1,a1) := b1 = (f2,a2) := b2 implies ( a1 = a2 & b1 = b2 & f1 = f2 ) )
A1: ( <*b1,f1,a1*> . 1 = b1 & <*b1,f1,a1*> . 2 = f1 ) ;
A2: ( <*b1,f1,a1*> . 3 = a1 & <*b2,f2,a2*> . 1 = b2 ) ;
A3: ( <*b2,f2,a2*> . 2 = f2 & <*b2,f2,a2*> . 3 = a2 ) ;
assume (f1,a1) := b1 = (f2,a2) := b2 ; :: thesis: ( a1 = a2 & b1 = b2 & f1 = f2 )
hence ( a1 = a2 & b1 = b2 & f1 = f2 ) by A1, A2, A3, XTUPLE_0:3; :: thesis: verum