deffunc H₁( Nat) -> FinSequence of the carrier of K * = 1. (K,(f . $1));
consider IT being FinSequence such that
A1: len IT = len f and
A2: for k being Nat st k in dom IT holds
IT . k = H₁(k) from FINSEQ_1:sch 2();
rng IT c= ( the carrier of K *) *

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng IT or y in ( the carrier of K *) * )
assume y in rng IT ; :: thesis: y in ( the carrier of K *) *
then consider x being object such that
A3: x in dom IT and
A4: IT . x = y by FUNCT_1:def 3;
reconsider x = x as Nat by A3;
IT . x = 1. (K,(f . x)) by A2, A3;
hence y in ( the carrier of K *) * by A4, FINSEQ_1:def 11; :: thesis: verum

end;

then reconsider IT = IT as FinSequence of ( the carrier of K *) * by FINSEQ_1:def 4;

now :: thesis: for i being Nat st i in dom IT holds
IT . i is Matrix of K

let i be Nat; :: thesis: ( i in dom IT implies IT . i is Matrix of K )
assume i in dom IT ; :: thesis: IT . i is Matrix of K
then IT . i = 1. (K,(f . i)) by A2;
hence IT . i is Matrix of K ; :: thesis: verum

end;

then reconsider IT = IT as FinSequence_of_Matrix of K by Def2;

now :: thesis: for i being Nat st i in dom IT holds
ex n being Nat st IT . i is Matrix of n,K

let i be Nat; :: thesis: ( i in dom IT implies ex n being Nat st IT . i is Matrix of n,K )
assume i in dom IT ; :: thesis: ex n being Nat st IT . i is Matrix of n,K
then IT . i = 1. (K,(f . i)) by A2;
hence ex n being Nat st IT . i is Matrix of n,K ; :: thesis: verum

end;

then reconsider IT = IT as FinSequence_of_Square-Matrix of K by Def6;
take IT ; :: thesis: ( dom IT = dom f & ( for i being Nat st i in dom IT holds
IT . i = 1. (K,(f . i)) ) )
thus ( dom IT = dom f & ( for i being Nat st i in dom IT holds
IT . i = 1. (K,(f . i)) ) ) by A1, A2, FINSEQ_3:29; :: thesis: verum