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 and

A6: for j being Nat st j in dom L1 holds

L1 . j = (M * (i,j)) * (Cofactor (M,i,j)) and

A7: len L2 = n and

A8: for j being Nat st j in dom L2 holds

L2 . j = (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;

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 and

A6: for j being Nat st j in dom L1 holds

L1 . j = (M * (i,j)) * (Cofactor (M,i,j)) and

A7: len L2 = n and

A8: for j being Nat st j in dom L2 holds

L2 . j = (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

hence
L1 = L2
by A10, A9, FINSEQ_1:13; :: thesis: verumL1 . 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 * (i,k)) * (Cofactor (M,i,k)) by A6, A11;

hence L1 . k = L2 . k by A8, A10, A9, A11; :: thesis: verum

end;assume A11: k in dom L1 ; :: thesis: L1 . k = L2 . k

L1 . k = (M * (i,k)) * (Cofactor (M,i,k)) by A6, A11;

hence L1 . k = L2 . k by A8, A10, A9, A11; :: thesis: verum