let K be Field; :: thesis: for A being Matrix of K
for i being Nat st len A > 1 holds
width A = width (DelLine (A,i))
let A be Matrix of K; :: thesis: for i being Nat st len A > 1 holds
width A = width (DelLine (A,i))
let i be Nat; :: thesis: ( len A > 1 implies width A = width (DelLine (A,i)) )
assume A1: len A > 1 ; :: thesis: width A = width (DelLine (A,i))

per cases ( i in dom A or not i in dom A ) ;

suppose i in dom A ; :: thesis: width A = width (DelLine (A,i))

then consider m being Nat such that
A2: len A = m + 1 and
A3: len (Del (A,i)) = m by FINSEQ_3:104;
A4: m >= 1 by A1, A2, NAT_1:13;
then A5: m in dom (Del (A,i)) by A3, FINSEQ_3:25;
then A6: (DelLine (A,i)) . m in rng (Del (A,i)) by FUNCT_1:def 3;
A7: rng (Del (A,i)) c= rng A by FINSEQ_3:106;
A8: (DelLine (A,i)) . m = Line ((DelLine (A,i)),m) by A5, MATRIX_0:60;
A is Matrix of len A, width A,K by A1, MATRIX_0:20;
then len (Line ((DelLine (A,i)),m)) = width A by A6, A8, A7, MATRIX_0:def 2;
hence width A = width (DelLine (A,i)) by A3, A4, A6, A8, MATRIX_0:def 3; :: thesis: verum

end;

suppose not i in dom A ; :: thesis: width A = width (DelLine (A,i))

hence width A = width (DelLine (A,i)) by FINSEQ_3:104; :: thesis: verum

end;

end;