deffunc H₁( Nat) -> FinSequence of INT.Ring = (f . (b1 /. $1)) |-- b2;
consider M being FinSequence such that
A1: len M = len b1 and
A2: for k being Nat st k in dom M holds
M . k = H₁(k) from FINSEQ_1:sch 2();
A3: dom M = Seg (len b1) by A1, FINSEQ_1:def 3;
ex n being Nat st
for x being object st x in rng M holds
ex s being FinSequence st
( s = x & len s = n )

proof

take n = len ((f . (b1 /. 1)) |-- b2); :: thesis: for x being object st x in rng M holds
ex s being FinSequence st
( s = x & len s = n )
let x be object ; :: thesis: ( x in rng M implies ex s being FinSequence st
( s = x & len s = n ) )
assume x in rng M ; :: thesis: ex s being FinSequence st
( s = x & len s = n )
then consider y being object such that
A4: y in dom M and
A5: x = M . y by FUNCT_1:def 3;
reconsider y = y as Nat by A4;
M . y = (f . (b1 /. y)) |-- b2 by A2, A4;
then reconsider s = M . y as FinSequence ;
take s ; :: thesis: ( s = x & len s = n )
thus s = x by A5; :: thesis: len s = n
thus len s = len ((f . (b1 /. y)) |-- b2) by A2, A4
.= len b2 by Def7
.= n by Def7 ; :: thesis: verum

end;

then reconsider M = M as tabular FinSequence by MATRIX_0:def 1;

now :: thesis: for x being object st x in rng M holds
x in INT *

let x be object ; :: thesis: ( x in rng M implies x in INT * )
assume x in rng M ; :: thesis: x in INT *
then consider y being object such that
A6: y in dom M and
A7: x = M . y by FUNCT_1:def 3;
reconsider y = y as Nat by A6;
M . y = (f . (b1 /. y)) |-- b2 by A2, A6;
then reconsider s = M . y as FinSequence of INT ;
s = x by A7;
hence x in INT * by FINSEQ_1:def 11; :: thesis: verum

end;

then rng M c= the carrier of INT.Ring * ;
then reconsider M = M as Matrix of INT.Ring by FINSEQ_1:def 4;
take M1 = M; :: thesis: ( len M1 = len b1 & ( for k being Nat st k in dom b1 holds
M1 /. k = (f . (b1 /. k)) |-- b2 ) )
for k being Nat st k in dom b1 holds
M1 /. k = (f . (b1 /. k)) |-- b2

proof

let k be Nat; :: thesis: ( k in dom b1 implies M1 /. k = (f . (b1 /. k)) |-- b2 )
assume A8: k in dom b1 ; :: thesis: M1 /. k = (f . (b1 /. k)) |-- b2
then A9: k in Seg (len b1) by FINSEQ_1:def 3;
dom M1 = dom b1 by A1, FINSEQ_3:29;
hence M1 /. k = M1 . k by A8, PARTFUN1:def 6
.= (f . (b1 /. k)) |-- b2 by A2, A3, A9 ;
:: thesis: verum

end;

hence ( len M1 = len b1 & ( for k being Nat st k in dom b1 holds
M1 /. k = (f . (b1 /. k)) |-- b2 ) ) by A1; :: thesis: verum