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:113;
A4: m >= 1 by A1, A2, NAT_1:13;
then A5: m in dom (Del A,i) by A3, FINSEQ_3:27;
then A6: (DelLine A,i) . m in rng (Del A,i) by FUNCT_1:def 5;
A7: rng (Del A,i) c= rng A by FINSEQ_3:115;
A8: (DelLine A,i) . m = Line (DelLine A,i),m by A5, MATRIX_2:18;
A is Matrix of len A, width A,K by A1, MATRIX_1:20;
then len (Line (DelLine A,i),m) = width A by A6, A8, A7, MATRIX_1:def 3;
hence width A = width (DelLine A,i) by A3, A4, A6, A8, MATRIX_1:def 4; :: 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:113; :: thesis: verum

end;

end;