deffunc H1( Nat) -> FinSequence of K = (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 = H1(k) from A3: dom M = Seg (len b1) by ;
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 ;
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 the carrier of K *
let x be object ; :: thesis: ( x in rng M implies x in the carrier of K * )
assume x in rng M ; :: thesis: x in the carrier of K *
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 ;
M . y = (f . (b1 /. y)) |-- b2 by A2, A6;
then reconsider s = M . y as FinSequence of K ;
s = x by A7;
hence x in the carrier of K * by FINSEQ_1:def 11; :: thesis: verum
end;
then rng M c= the carrier of K * ;
then reconsider M = M as Matrix of K 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 ;
hence M1 /. k = M1 . k by
.= (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