let L1, L2 be FinSequence of K; :: thesis: ( len L1 = n & ( for j being Nat st j in dom L1 holds
L1 . j = (M * i,j) * (Cofactor M,i,j) ) & len L2 = n & ( for j being Nat st j in dom L2 holds
L2 . j = (M * i,j) * (Cofactor M,i,j) ) implies L1 = L2 )
assume that
A5: ( len L1 = n & ( for j being Nat st j in dom L1 holds
L1 . j = (M * i,j) * (Cofactor M,i,j) ) ) and
A6: ( len L2 = n & ( for j being Nat st j in dom L2 holds
L2 . j = (M * i,j) * (Cofactor M,i,j) ) ) ; :: thesis: L1 = L2
A7: ( dom L1 = Seg n & dom L2 = Seg n ) by A5, A6, FINSEQ_1:def 3;

now

let k be Nat; :: thesis: ( k in dom L1 implies L1 . k = L2 . k )
assume A8: k in dom L1 ; :: thesis: L1 . k = L2 . k
( L1 . k = (M * i,k) * (Cofactor M,i,k) & L2 . k = (M * i,k) * (Cofactor M,i,k) ) by A5, A6, A7, A8;
hence L1 . k = L2 . k ; :: thesis: verum

end;

hence L1 = L2 by A7, FINSEQ_1:17; :: thesis: verum