deffunc H₁( Nat) -> Matrix of f . $1,f . $1,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();
A3: ( dom IT = Seg (len IT) & dom IT = dom f ) by A1, FINSEQ_1:def 3, FINSEQ_3:31;
rng IT c= (the carrier of K * ) *

proof

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

end;

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

now

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

end;

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

now

let i be Nat; :: thesis: ( i in dom IT implies ex n being Nat st IT . i is Matrix of n,K )
assume A7: i in dom IT ; :: thesis: ex n being Nat st IT . i is Matrix of n,K
IT . i = 1. K,(f . i) by A2, A7;
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 A2, A3; :: thesis: verum