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 ;
then A5: m in dom (Del (A,i)) by ;
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 ;
A is Matrix of len A, width A,K by ;
then len (Line ((DelLine (A,i)),m)) = width A by ;
hence width A = width (DelLine (A,i)) by ; :: 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;