let b1, a1, b2, a2 be Int-Location ; :: thesis: for f1, f2 being FinSeq-Location st b1 := f1,a1 = b2 := f2,a2 holds
( a1 = a2 & b1 = b2 & f1 = f2 )
let f1, f2 be FinSeq-Location ; :: thesis: ( b1 := f1,a1 = b2 := f2,a2 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 b1 := f1,a1 = b2 := f2,a2 ; :: thesis: ( a1 = a2 & b1 = b2 & f1 = f2 )
hence ( a1 = a2 & b1 = b2 & f1 = f2 ) by A1, A2, A3, MCART_1:28; :: thesis: verum