let L1, L2 be FinSequence of K; :: thesis:
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:
A9: dom L2 = Seg n by A7, FINSEQ_1:def 3;
A10: dom L1 = Seg n by A5, FINSEQ_1:def 3;

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

end;