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 *

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng p or x in REAL * )
assume x in rng p ; :: thesis: x in REAL *
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: verum

end;

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

proof

let x be object ; :: thesis: ( x in rng p implies ex q being FinSequence st
( q = x & len q = width MR ) )
assume x in rng p ; :: thesis: ex q being FinSequence st
( q = x & len q = width MR )
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: verum

end;

then reconsider p = p as Matrix of REAL by A4, FINSEQ_1:def 4, MATRIX_0:def 1;
take p ; :: thesis: ( 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))))) ) )
width p = width MR

proof

per cases ( len MR = 0 or len MR > 0 ) ;

suppose A12: len MR = 0 ; :: thesis: width p = width MR

then width p = 0 by A2, MATRIX_0:def 3;
hence width p = width MR by A12, MATRIX_0:def 3; :: thesis: verum

end;

suppose A13: len MR > 0 ; :: thesis: width p = width MR

then len p >= 1 by A2, NAT_1:14;
then 1 in Seg (len p) by FINSEQ_1:1;
then A14: 1 in dom p by FINSEQ_1:def 3;
then A15: p . 1 in rng p by FUNCT_1:3;
ex q being FinSequence st
( q = p . 1 & len q = width MR ) by A7, A14, FUNCT_1:3;
hence width p = width MR by A2, A13, A15, MATRIX_0:def 3; :: thesis: verum

end;

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: verum