let D be non empty set ; :: thesis: 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; :: thesis: for i being Nat st not i in Seg (width M) holds
DelCol (M,i) = M
let i be Nat; :: thesis: ( not i in Seg (width M) implies DelCol (M,i) = M )
assume A1: not i in Seg (width M) ; :: thesis: 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; :: thesis: ( 1 <= k & k <= len M implies M . k = (DelCol (M,i)) . k )
assume A3: ( 1 <= k & k <= len M ) ; :: thesis: 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 ; :: thesis: verum

end;

hence DelCol (M,i) = M by A2, FINSEQ_1:14; :: thesis: verum