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 )

take n = len ((f . (b1 /. 1)) |-- b2); :: thesis:
let x be object ; :: thesis:
assume x in rng M ; :: thesis:
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:
thus s = x by A5; :: thesis:
thus len s = len ((f . (b1 /. y)) |-- b2) by A2, A4
.= len b2 by Def7
.= n by Def7 ; :: thesis:

end;

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

let x be object ; :: thesis:
assume x in rng M ; :: thesis:
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:

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:
for k being Nat st k in dom b1 holds
M1 /. k = (f . (b1 /. k)) |-- b2

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: