let D be non empty set ; :: thesis: for n9, m9, i being Nat
for A9 being Matrix of n9,m9,D
for F being FinSequence of D st not i in Seg (len A9) holds
RLine A9,i,F = A9
let n9, m9, i be Nat; :: thesis: for A9 being Matrix of n9,m9,D
for F being FinSequence of D st not i in Seg (len A9) holds
RLine A9,i,F = A9
let A9 be Matrix of n9,m9,D; :: thesis: for F being FinSequence of D st not i in Seg (len A9) holds
RLine A9,i,F = A9
let F be FinSequence of D; :: thesis: ( not i in Seg (len A9) implies RLine A9,i,F = A9 )
assume A1: not i in Seg (len A9) ; :: thesis: RLine A9,i,F = A9
set R = RLine A9,i,F;

per cases ( len F = width A9 or len F <> width A9 ) ;

suppose A2: len F = width A9 ; :: thesis: RLine A9,i,F = A9

A3: now

let k be Nat; :: thesis: ( 1 <= k & k <= len A9 implies (RLine A9,i,F) . k = A9 . k )
assume that
A4: 1 <= k and
A5: k <= len A9 ; :: thesis: (RLine A9,i,F) . k = A9 . k
k in NAT by ORDINAL1:def 13;
then A6: k in Seg (len A9) by A4, A5;
A7: len A9 = n9 by MATRIX_1:def 3;
then A8: (RLine A9,i,F) . k = Line (RLine A9,i,F),k by A6, MATRIX_2:10;
Line (RLine A9,i,F),k = Line A9,k by A1, A6, A7, MATRIX11:28;
hence (RLine A9,i,F) . k = A9 . k by A6, A7, A8, MATRIX_2:10; :: thesis: verum

end;

len A9 = len (RLine A9,i,F) by A2, MATRIX11:def 3;
hence RLine A9,i,F = A9 by A3, FINSEQ_1:18; :: thesis: verum

end;

suppose len F <> width A9 ; :: thesis: RLine A9,i,F = A9

hence RLine A9,i,F = A9 by MATRIX11:def 3; :: thesis: verum

end;

end;