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 K 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 MATRIX_1:def 8;
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:113 ; :: thesis: verum

end;

suppose A4: i in Seg (width M) ; :: thesis: ex b₁ being Matrix of K 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 K] means $3 = (Del (Line M,$1),i) . $2;

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

suppose len M = 0 ; :: thesis: ex b₁ being Matrix of K 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 K st
( len b₁ = len M & ( for k being Nat st k in dom M holds
b₁ . k = Del (Line M,k),i ) ) by A4, FINSEQ_1:4, MATRIX_1:def 4; :: thesis: verum

end;

suppose A5: len M > 0 ; :: thesis: ex b₁ being Matrix of K 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 K 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 K 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 K 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
A6: width M = m + 1 by NAT_1:6;
reconsider m = m as Element of NAT by ORDINAL1:def 13;
A7: 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
A8: len (Line M,k) = width M by MATRIX_1:def 8;
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:113;
hence len (Del (Line M,k),i) = m by A6, A8; :: thesis: verum

end;

A9: for k, l being Nat st [k,l] in [:(Seg (len M)),(Seg m):] holds
for x1, x2 being Element of K st S₁[k,l,x1] & S₁[k,l,x2] holds
x1 = x2 ;
A10: for k, l being Nat st [k,l] in [:(Seg (len M)),(Seg m):] holds
ex x being Element of K 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 K st S₁[k,l,x] )
assume A11: [k,l] in [:(Seg (len M)),(Seg m):] ; :: thesis: ex x being Element of K st S₁[k,l,x]
dom M = Seg (len M) by FINSEQ_1:def 3;
then A12: ( k in dom M & l in Seg m ) by A11, ZFMISC_1:106;
reconsider p = Del (Line M,k),i as FinSequence of K by FINSEQ_3:114;
A13: len p = m by A7, A12;
dom p = Seg (len p) by FINSEQ_1:def 3;
then reconsider x = p . l as Element of the carrier of K by A12, A13, FINSEQ_2:13;
take x ; :: thesis: S₁[k,l,x]
thus S₁[k,l,x] ; :: thesis: verum

end;

consider N being Matrix of len M,m,K such that
A14: for k, l being Nat st [k,l] in Indices N holds
S₁[k,l,N * k,l] from MATRIX_1:sch 2(A9, A10);
dom M = Seg (len M) by FINSEQ_1:def 3;
then A15: ( len N = len M & width N = m & Indices N = [:(dom M),(Seg m):] ) by A5, MATRIX_1:24;
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:106;
hence N * k,l = (Del (Line M,k),i) . l by A14; :: thesis: verum

end;

reconsider N = N as Matrix of K ;
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 A17: k in dom M ; :: thesis: N . k = Del (Line M,k),i
then k in Seg (len M) by FINSEQ_1:def 3;
then A18: N . k = Line N,k by Th10;
then reconsider s = N . k as FinSequence ;
A19: len s = m by A15, A18, MATRIX_1:def 8;
A20: len (Del (Line M,k),i) = m by A7, A17;
X: dom s = Seg m by A19, FINSEQ_1:def 3;

now

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

end;

hence N . k = Del (Line M,k),i by A19, A20, FINSEQ_2:10; :: 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 A5, MATRIX_1:24; :: thesis: verum

end;

end;

end;

end;

end;

end;