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