let D be non empty set ; for M being Matrix of D
for i being Nat st not i in Seg (width M) holds
DelCol (M,i) = M
let M be Matrix of D; for i being Nat st not i in Seg (width M) holds
DelCol (M,i) = M
let i be Nat; ( not i in Seg (width M) implies DelCol (M,i) = M )
assume A1:
not i in Seg (width M)
; DelCol (M,i) = M
A2:
len (DelCol (M,i)) = len M
by Def13;
for k being Nat st 1 <= k & k <= len M holds
M . k = (DelCol (M,i)) . k
proof
let k be
Nat;
( 1 <= k & k <= len M implies M . k = (DelCol (M,i)) . k )
assume A3:
( 1
<= k &
k <= len M )
;
M . k = (DelCol (M,i)) . k
A4:
k in dom M
by A3, FINSEQ_3:25;
len (Line (M,k)) = width M
by Def7;
then A5:
not
i in dom (Line (M,k))
by A1, FINSEQ_1:def 3;
thus M . k =
Line (
M,
k)
by A4, Lm1
.=
Del (
(Line (M,k)),
i)
by A5, FINSEQ_3:104
.=
(DelCol (M,i)) . k
by A4, Def13
;
verum
end;
hence
DelCol (M,i) = M
by A2, FINSEQ_1:14; verum