deffunc H₁( Nat) -> FinSequence of the carrier of K * = (G1 . $1) + (G2 . $1);
consider IT being FinSequence such that
A1: len IT = len G1 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 = (G1 . x) + (G2 . 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 = (G1 . i) + (G2 . 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;
take IT ; :: thesis: ( dom IT = dom G1 & ( for i being Nat st i in dom IT holds
IT . i = (G1 . i) + (G2 . i) ) )
thus ( dom IT = dom G1 & ( for i being Nat st i in dom IT holds
IT . i = (G1 . i) + (G2 . i) ) ) by A1, A2, FINSEQ_3:29; :: thesis: verum