let M be Matrix of 3,F_Real; :: thesis: for x being object holds
( x in lines (M @) iff ex i being Nat st
( i in Seg 3 & x = Col (M,i) ) )
let x be object ; :: thesis: ( x in lines (M @) iff ex i being Nat st
( i in Seg 3 & x = Col (M,i) ) )

hereby :: thesis: ( ex i being Nat st
( i in Seg 3 & x = Col (M,i) ) implies x in lines (M @) )

assume x in lines (M @) ; :: thesis: ex i being Nat st
( i in Seg 3 & x = Col (M,i) )
then consider i being Nat such that
A1: i in Seg 3 and
A2: x = Line ((M @),i) by MATRIX13:103;
i in Seg (width M) by A1, MATRIX_0:24;
then x = Col (M,i) by A2, MATRIX_0:59;
hence ex i being Nat st
( i in Seg 3 & x = Col (M,i) ) by A1; :: thesis: verum

end;

given i being Nat such that A3: i in Seg 3 and
A4: x = Col (M,i) ; :: thesis: x in lines (M @)
i in Seg (width M) by A3, MATRIX_0:24;
then x = Line ((M @),i) by A4, MATRIX_0:59;
hence x in lines (M @) by A3, MATRIX13:103; :: thesis: verum