reconsider N = n as Element of NAT by ORDINAL1:def 12;
deffunc H₁( Nat) -> Element of the carrier of K = (M * (i,$1)) * (Cofactor (M,i,$1));
consider LL being FinSequence such that
A1: ( len LL = N & ( for k being Nat st k in dom LL holds
LL . k = H₁(k) ) ) from FINSEQ_1:sch 2();
rng LL c= the carrier of K

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng LL or x in the carrier of K )
assume x in rng LL ; :: thesis: x in the carrier of K
then consider y being object such that
A2: y in dom LL and
A3: LL . y = x by FUNCT_1:def 3;
dom LL = Seg n by A1, FINSEQ_1:def 3;
then consider k being Nat such that
A4: k = y and
1 <= k and
k <= n by A2;
H₁(k) is Element of K ;
then LL . k is Element of K by A1, A2, A4;
hence x in the carrier of K by A3, A4; :: thesis: verum

end;

then reconsider LL = LL as FinSequence of K by FINSEQ_1:def 4;
take LL ; :: thesis: ( len LL = n & ( for j being Nat st j in dom LL holds
LL . j = (M * (i,j)) * (Cofactor (M,i,j)) ) )
thus len LL = n by A1; :: thesis: for j being Nat st j in dom LL holds
LL . j = (M * (i,j)) * (Cofactor (M,i,j))
thus for j being Nat st j in dom LL holds
LL . j = (M * (i,j)) * (Cofactor (M,i,j)) by A1; :: thesis: verum