deffunc H₁( Nat) -> FinSequence of REAL = mlt ((Line (MR,$1)),(FinSeq_log (2,(Line (MR,$1)))));
consider p being FinSequence such that
A2: len p = len MR and
A3: for k being Nat st k in dom p holds
p . k = H₁(k) from FINSEQ_1:sch 2();
A4: rng p c= REAL *

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in rng p ; :: thesis:
then consider j being Nat such that
A5: j in dom p and
A6: x = p . j by FINSEQ_2:10;
p . j = mlt ((Line (MR,j)),(FinSeq_log (2,(Line (MR,j))))) by A3, A5;
hence x in REAL * by A6, FINSEQ_1:def 11; :: thesis:

end;

A7: for x being object st x in rng p holds
ex q being FinSequence st
( q = x & len q = width MR )

let x be object ; :: thesis:
assume x in rng p ; :: thesis:
then consider j being Nat such that
A8: j in dom p and
A9: x = p . j by FINSEQ_2:10;
j in dom MR by A2, A8, FINSEQ_3:29;
then Line (MR,j) is nonnegative by A1, Th19;
then A10: len (FinSeq_log (2,(Line (MR,j)))) = len (Line (MR,j)) by Def6;
len (Line (MR,j)) = width MR by MATRIX_0:def 7;
then A11: len (mlt ((Line (MR,j)),(FinSeq_log (2,(Line (MR,j)))))) = width MR by A10, MATRPROB:30;
x = mlt ((Line (MR,j)),(FinSeq_log (2,(Line (MR,j))))) by A3, A8, A9;
hence ex q being FinSequence st
( q = x & len q = width MR ) by A11; :: thesis:

end;

then reconsider p = p as Matrix of REAL by A4, FINSEQ_1:def 4, MATRIX_0:def 1;
take p ; :: thesis:
width p = width MR

end;

end;

hence ( len p = len MR & width p = width MR & ( for k being Nat st k in dom p holds
p . k = mlt ((Line (MR,k)),(FinSeq_log (2,(Line (MR,k))))) ) ) by A2, A3; :: thesis: