let x be object ; :: thesis: for m, n being Nat
for K being Field
for M being Matrix of m,n,K holds
( x in lines M iff ex i being Nat st
( i in Seg m & x = Line (M,i) ) )
let m, n be Nat; :: thesis: for K being Field
for M being Matrix of m,n,K holds
( x in lines M iff ex i being Nat st
( i in Seg m & x = Line (M,i) ) )
let K be Field; :: thesis: for M being Matrix of m,n,K holds
( x in lines M iff ex i being Nat st
( i in Seg m & x = Line (M,i) ) )
let M be Matrix of m,n,K; :: thesis: ( x in lines M iff ex i being Nat st
( i in Seg m & x = Line (M,i) ) )
thus ( x in lines M implies ex i being Nat st
( i in Seg m & x = Line (M,i) ) ) :: thesis: ( ex i being Nat st
( i in Seg m & x = Line (M,i) ) implies x in lines M )

proof

assume x in lines M ; :: thesis: ex i being Nat st
( i in Seg m & x = Line (M,i) )
then consider i being object such that
A1: i in dom M and
A2: M . i = x by FUNCT_1:def 3;
A3: len M = m by MATRIX_0:def 2;
reconsider i = i as Element of NAT by A1;
A4: dom M = Seg (len M) by FINSEQ_1:def 3;
then M . i = Line (M,i) by A1, A3, MATRIX_0:52;
hence ex i being Nat st
( i in Seg m & x = Line (M,i) ) by A1, A2, A4, A3; :: thesis: verum

end;

given i being Nat such that A5: i in Seg m and
A6: x = Line (M,i) ; :: thesis: x in lines M
A7: len M = m by MATRIX_0:def 2;
dom M = Seg (len M) by FINSEQ_1:def 3;
then M . i in rng M by A5, A7, FUNCT_1:def 3;
hence x in lines M by A5, A6, MATRIX_0:52; :: thesis: verum