reconsider N = n as Element of NAT by ORDINAL1:def 12;

deffunc H_{1}( 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 = H_{1}(k) ) )
from FINSEQ_1:sch 2();

rng LL c= the carrier of K

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

deffunc H

consider LL being FinSequence such that

A1: ( len LL = N & ( for k being Nat st k in dom LL holds

LL . k = H

rng LL c= the carrier of K

proof

then reconsider LL = LL as FinSequence of K by FINSEQ_1:def 4;
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_{1}(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;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

then LL . k is Element of K by A1, A2, A4;

hence x in the carrier of K by A3, A4; :: thesis: verum

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