per cases ( not i in Seg (width M) or i in Seg (width M) ) ;

suppose A1: not i in Seg (width M) ; :: thesis: ex b₁ being Matrix of D st
( len b₁ = len M & ( for k being Nat st k in dom M holds
b₁ . k = Del ((Line (M,k)),i) ) )

take M ; :: thesis: ( len M = len M & ( for k being Nat st k in dom M holds
M . k = Del ((Line (M,k)),i) ) )
thus len M = len M ; :: thesis: for k being Nat st k in dom M holds
M . k = Del ((Line (M,k)),i)
let k be Nat; :: thesis: ( k in dom M implies M . k = Del ((Line (M,k)),i) )
assume A2: k in dom M ; :: thesis: M . k = Del ((Line (M,k)),i)
len (Line (M,k)) = width M by Def7;
then A3: not i in dom (Line (M,k)) by A1, FINSEQ_1:def 3;
thus M . k = Line (M,k) by A2, Lm1
.= Del ((Line (M,k)),i) by A3, FINSEQ_3:104 ; :: thesis: verum

end;

suppose A4: i in Seg (width M) ; :: thesis: ex b₁ being Matrix of D st
( len b₁ = len M & ( for k being Nat st k in dom M holds
b₁ . k = Del ((Line (M,k)),i) ) )

defpred S₁[ Nat, Nat, Element of D] means $3 = (Del ((Line (M,$1)),i)) . $2;

per cases ( len M = 0 or len M > 0 ) ;

suppose A5: len M = 0 ; :: thesis: ex b₁ being Matrix of D st
( len b₁ = len M & ( for k being Nat st k in dom M holds
b₁ . k = Del ((Line (M,k)),i) ) )

then Seg (len M) = {} ;
hence ex b₁ being Matrix of D st
( len b₁ = len M & ( for k being Nat st k in dom M holds
b₁ . k = Del ((Line (M,k)),i) ) ) by A4, A5, Def3; :: thesis: verum

end;

suppose A6: len M > 0 ; :: thesis: ex b₁ being Matrix of D st
( len b₁ = len M & ( for k being Nat st k in dom M holds
b₁ . k = Del ((Line (M,k)),i) ) )

set n1 = width M;

per cases ( width M = 0 or width M > 0 ) ;

suppose width M = 0 ; :: thesis: ex b₁ being Matrix of D st
( len b₁ = len M & ( for k being Nat st k in dom M holds
b₁ . k = Del ((Line (M,k)),i) ) )

hence ex b₁ being Matrix of D st
( len b₁ = len M & ( for k being Nat st k in dom M holds
b₁ . k = Del ((Line (M,k)),i) ) ) by A4; :: thesis: verum

end;

suppose width M > 0 ; :: thesis: ex b₁ being Matrix of D st
( len b₁ = len M & ( for k being Nat st k in dom M holds
b₁ . k = Del ((Line (M,k)),i) ) )

then consider m being Nat such that
A7: width M = m + 1 by NAT_1:6;
reconsider m = m as Nat ;
A8: for k being Nat st k in dom M holds
len (Del ((Line (M,k)),i)) = m

proof

let k be Nat; :: thesis: ( k in dom M implies len (Del ((Line (M,k)),i)) = m )
assume k in dom M ; :: thesis: len (Del ((Line (M,k)),i)) = m
A9: len (Line (M,k)) = width M by Def7;
then i in dom (Line (M,k)) by A4, FINSEQ_1:def 3;
then ex l being Nat st
( len (Line (M,k)) = l + 1 & len (Del ((Line (M,k)),i)) = l ) by FINSEQ_3:104;
hence len (Del ((Line (M,k)),i)) = m by A7, A9; :: thesis: verum

end;

A10: for k, l being Nat st [k,l] in [:(Seg (len M)),(Seg m):] holds
ex x being Element of D st S₁[k,l,x]

proof

let k, l be Nat; :: thesis: ( [k,l] in [:(Seg (len M)),(Seg m):] implies ex x being Element of D st S₁[k,l,x] )
assume A11: [k,l] in [:(Seg (len M)),(Seg m):] ; :: thesis: ex x being Element of D st S₁[k,l,x]
reconsider p = Del ((Line (M,k)),i) as FinSequence of D by FINSEQ_3:105;
dom M = Seg (len M) by FINSEQ_1:def 3;
then k in dom M by A11, ZFMISC_1:87;
then A12: len p = m by A8;
A13: dom p = Seg (len p) by FINSEQ_1:def 3;
l in Seg m by A11, ZFMISC_1:87;
then reconsider x = p . l as Element of D by A12, A13, FINSEQ_2:11;
take x ; :: thesis: S₁[k,l,x]
thus S₁[k,l,x] ; :: thesis: verum

end;

consider N being Matrix of len M,m,D such that
A14: for k, l being Nat st [k,l] in Indices N holds
S₁[k,l,N * (k,l)] from MATRIX_0:sch 2(A10);
dom M = Seg (len M) by FINSEQ_1:def 3;
then A15: Indices N = [:(dom M),(Seg m):] by A6, Th23;
A16: for k, l being Nat st k in dom M & l in Seg m holds
N * (k,l) = (Del ((Line (M,k)),i)) . l

proof

let k, l be Nat; :: thesis: ( k in dom M & l in Seg m implies N * (k,l) = (Del ((Line (M,k)),i)) . l )
assume ( k in dom M & l in Seg m ) ; :: thesis: N * (k,l) = (Del ((Line (M,k)),i)) . l
then [k,l] in Indices N by A15, ZFMISC_1:87;
hence N * (k,l) = (Del ((Line (M,k)),i)) . l by A14; :: thesis: verum

end;

A17: width N = m by A6, Th23;
reconsider N = N as Matrix of D ;
take N ; :: thesis: ( len N = len M & ( for k being Nat st k in dom M holds
N . k = Del ((Line (M,k)),i) ) )
for k being Nat st k in dom M holds
N . k = Del ((Line (M,k)),i)

proof

let k be Nat; :: thesis: ( k in dom M implies N . k = Del ((Line (M,k)),i) )
assume A18: k in dom M ; :: thesis: N . k = Del ((Line (M,k)),i)
then k in Seg (len M) by FINSEQ_1:def 3;
then A19: N . k = Line (N,k) by Th52;
reconsider s = N . k as FinSequence ;
A20: len s = m by A17, A19, Def7;
then A21: dom s = Seg m by FINSEQ_1:def 3;

A22: now :: thesis: for j being Nat st j in dom s holds
s . j = (Del ((Line (M,k)),i)) . j

let j be Nat; :: thesis: ( j in dom s implies s . j = (Del ((Line (M,k)),i)) . j )
assume A23: j in dom s ; :: thesis: s . j = (Del ((Line (M,k)),i)) . j
then (Line (N,k)) . j = N * (k,j) by A17, A21, Def7;
hence s . j = (Del ((Line (M,k)),i)) . j by A16, A18, A19, A21, A23; :: thesis: verum

end;

len (Del ((Line (M,k)),i)) = m by A8, A18;
hence N . k = Del ((Line (M,k)),i) by A20, A22, FINSEQ_2:9; :: thesis: verum

end;

hence ( len N = len M & ( for k being Nat st k in dom M holds
N . k = Del ((Line (M,k)),i) ) ) by A6, Th23; :: thesis: verum

end;

end;

end;

end;

end;

end;