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 FINSEQ_1:sch 2();
rng LL c= the carrier of K
then reconsider LL = LL as FinSequence of K by FINSEQ_1:def 4;
take
LL
; ( 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; for i being Nat st i in dom LL holds
LL . i = (M * (i,j)) * (Cofactor (M,i,j))
let i be Nat; ( i in dom LL implies LL . i = (M * (i,j)) * (Cofactor (M,i,j)) )
assume
i in dom LL
; LL . i = (M * (i,j)) * (Cofactor (M,i,j))
hence
LL . i = (M * (i,j)) * (Cofactor (M,i,j))
by A1; verum