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 set ; :: 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:11;
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 set st x in rng p holds
ex q being FinSequence st
( q = x & len q = width MR )

proof

set n = width MR;
let x be set ; :: 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:11;
j in dom MR by A2, A8, FINSEQ_3:31;
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_1:def 8;
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_1:def 1;
take p ; :: thesis: ( len p = len MR & width p = width MR & ( for k being Element of 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_1:def 4;
hence width p = width MR by A12, MATRIX_1:def 4; :: 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:3;
then A14: 1 in dom p by FINSEQ_1:def 3;
then A15: p . 1 in rng p by FUNCT_1:12;
ex q being FinSequence st
( q = p . 1 & len q = width MR ) by A7, A14, FUNCT_1:12;
hence width p = width MR by A2, A13, A15, MATRIX_1:def 4; :: thesis: verum

end;

end;

end;

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