let K be Field; 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; for i being Nat st len A > 1 holds
width A = width (DelLine (A,i))
let i be Nat; ( len A > 1 implies width A = width (DelLine (A,i)) )
assume A1:
len A > 1
; width A = width (DelLine (A,i))
per cases
( i in dom A or not i in dom A )
;
suppose
i in dom A
;
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;
verum end;