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 :: thesis: for k being Nat st k in dom L1 holds
L1 . k = L2 . k

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:13; :: thesis: verum