let D be non empty set ; :: thesis: for i being Nat
for A being Matrix of D st 1 <= i & i <= len A holds
Line (A,i) = A . i
let i be Nat; :: thesis: for A being Matrix of D st 1 <= i & i <= len A holds
Line (A,i) = A . i
let A be Matrix of D; :: thesis: ( 1 <= i & i <= len A implies Line (A,i) = A . i )
assume ( 1 <= i & i <= len A ) ; :: thesis: Line (A,i) = A . i
then i in dom A by FINSEQ_3:25;
hence Line (A,i) = A . i by MATRIX_0:60; :: thesis: verum