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

now

let k be Nat; :: thesis: ( k in dom L1 implies L1 . k = L2 . k )
assume A11: k in dom L1 ; :: thesis: L1 . k = L2 . k
L1 . k = (M * k,j) * (Cofactor M,k,j) by A6, A11;
hence L1 . k = L2 . k by A8, A10, A9, A11; :: thesis: verum

end;

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