reconsider N = n as Element of NAT by ORDINAL1:def 12;
deffunc H1( Nat) -> Element of the carrier of K = (M * (\$1,j)) * (Cofactor (M,\$1,j));
consider LL being FinSequence such that
A1: ( len LL = N & ( for k being Nat st k in dom LL holds
LL . k = H1(k) ) ) from 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 ;
then consider k being Nat such that
A4: k = y and
1 <= k and
k <= n by A2;
H1(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 i being Nat st i in dom LL holds
LL . i = (M * (i,j)) * (Cofactor (M,i,j)) ) )

thus len LL = n by A1; :: thesis: for i being Nat st i in dom LL holds
LL . i = (M * (i,j)) * (Cofactor (M,i,j))

let i be Nat; :: thesis: ( i in dom LL implies LL . i = (M * (i,j)) * (Cofactor (M,i,j)) )
assume i in dom LL ; :: thesis: LL . i = (M * (i,j)) * (Cofactor (M,i,j))
hence LL . i = (M * (i,j)) * (Cofactor (M,i,j)) by A1; :: thesis: verum