let D be non empty set ; :: thesis: for i, m9, n9 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 i, m9, n9 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 :: thesis: for k being Nat st 1 <= k & k <= len A9 holds
(RLine (A9,i,F)) . k = A9 . k

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
A6: k in Seg (len A9) by A4, A5;
A7: len A9 = n9 by MATRIX_0:def 2;
then A8: (RLine (A9,i,F)) . k = Line ((RLine (A9,i,F)),k) by A6, MATRIX_0:52;
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_0:52; :: thesis: verum

end;

len A9 = len (RLine (A9,i,F)) by A2, MATRIX11:def 3;
hence RLine (A9,i,F) = A9 by A3; :: 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;