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 S: 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 ) )

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

end;

A13: 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 ;
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(A13, A9);
dom M = Seg (len M) by FINSEQ_1:def 3;
then A15: 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;

A17: width N = m by A5, MATRIX_1:24;
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 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 Th10;
then reconsider s = N . k as FinSequence ;
A20: len s = m by A17, A19, MATRIX_1:def 8;
then A21: dom s = Seg m by FINSEQ_1:def 3;

A22: now

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, MATRIX_1:def 8;
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 A7, A18;
hence N . k = Del (Line M,k),i by A20, A22, 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;