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 len F = width A' ; :: thesis: RLine A',i,F = A'

then A2: len A' = len (RLine A',i,F) by MATRIX11:def 3;

now

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

end;

hence RLine A',i,F = A' by A2, 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;