let a1, b1, a2, 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 ) by FINSEQ_1:62;
A2: ( <*b1,f1,a1*> . 3 = a1 & <*b2,f2,a2*> . 1 = b2 ) by FINSEQ_1:62;
A3: ( <*b2,f2,a2*> . 2 = f2 & <*b2,f2,a2*> . 3 = a2 ) by FINSEQ_1:62;
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, ZFMISC_1:33; :: thesis: verum