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

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

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

A3: now

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

end;

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

end;

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

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

end;

end;