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

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 )
;

end;

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;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