deffunc H_{1}( 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 = H_{1}(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 )

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

M1 /. k = (f . (b1 /. k)) |-- b2 ) ) by A1; :: thesis: verum

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

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

then reconsider M = M as tabular FinSequence by MATRIX_0:def 1;
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, FINSEQ_3:23;

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;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, FINSEQ_3:23;

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

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

x in the carrier of K *

then
rng M c= the carrier of K *
;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 A6, FINSEQ_3:23;

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;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 A6, FINSEQ_3:23;

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

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

hence
( len M1 = len b1 & ( for k being Nat st k in dom b1 holds
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;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

M1 /. k = (f . (b1 /. k)) |-- b2 ) ) by A1; :: thesis: verum