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
A6: ( len L1 = n & ( for i being Nat st i in dom L1 holds
L1 . i = (M * i,j) * (Cofactor M,i,j) ) ) and
A7: ( len L2 = n & ( for i being Nat st i in dom L2 holds
L2 . i = (M * i,j) * (Cofactor M,i,j) ) ) ; :: thesis: L1 = L2
A8: ( dom L1 = Seg n & dom L2 = Seg n ) by A6, A7, FINSEQ_1:def 3;

now

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

end;

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