let D be non empty set ; :: thesis: for G being Matrix of D
for i, k, m being Nat st i in Seg (width G) & width G = m + 1 & m > 0 & 1 <= k & k < i holds
( Col ((DelCol (G,i)),k) = Col (G,k) & k in Seg (width (DelCol (G,i))) & k in Seg (width G) )
let G be Matrix of D; :: thesis: for i, k, m being Nat st i in Seg (width G) & width G = m + 1 & m > 0 & 1 <= k & k < i holds
( Col ((DelCol (G,i)),k) = Col (G,k) & k in Seg (width (DelCol (G,i))) & k in Seg (width G) )
let i, k, m be Nat; :: thesis: ( i in Seg (width G) & width G = m + 1 & m > 0 & 1 <= k & k < i implies ( Col ((DelCol (G,i)),k) = Col (G,k) & k in Seg (width (DelCol (G,i))) & k in Seg (width G) ) )
set N = DelCol (G,i);
assume that
A1: i in Seg (width G) and
A2: width G = m + 1 and
A3: m > 0 and
A4: 1 <= k and
A5: k < i ; :: thesis: ( Col ((DelCol (G,i)),k) = Col (G,k) & k in Seg (width (DelCol (G,i))) & k in Seg (width G) )
A6: width (DelCol (G,i)) = m by A1, A2, Th63;
A7: 1 < width G by A2, A3, SEQM_3:43;
A8: len (DelCol (G,i)) = len G by Def13;
i <= m + 1 by A1, A2, FINSEQ_1:1;
then A9: k < m + 1 by A5, XXREAL_0:2;
then A10: k in Seg (width G) by A2, A4, FINSEQ_1:1;
A11: len (Col (G,k)) = len G by Def8;
A12: len (Col ((DelCol (G,i)),k)) = len (DelCol (G,i)) by Def8;
A13: k <= m by A9, NAT_1:13;
then A14: k in Seg (width (DelCol (G,i))) by A4, A6, FINSEQ_1:1;

now :: thesis: for j being Nat st 1 <= j & j <= len (Col ((DelCol (G,i)),k)) holds
(Col ((DelCol (G,i)),k)) . j = (Col (G,k)) . j

let j be Nat; :: thesis: ( 1 <= j & j <= len (Col ((DelCol (G,i)),k)) implies (Col ((DelCol (G,i)),k)) . j = (Col (G,k)) . j )
A15: ( dom (DelCol (G,i)) = Seg (len (DelCol (G,i))) & dom G = Seg (len G) ) by FINSEQ_1:def 3;
assume ( 1 <= j & j <= len (Col ((DelCol (G,i)),k)) ) ; :: thesis: (Col ((DelCol (G,i)),k)) . j = (Col (G,k)) . j
then A16: j in dom (DelCol (G,i)) by A12, FINSEQ_3:25;
hence (Col ((DelCol (G,i)),k)) . j = (DelCol (G,i)) * (j,k) by Def8
.= (Del ((Line (G,j)),i)) . k by A1, A14, A7, A8, A16, A15, Th66
.= (Line (G,j)) . k by A5, FINSEQ_3:110
.= (Col (G,k)) . j by A10, A8, A16, A15, Th42 ;
:: thesis: verum

end;

hence ( Col ((DelCol (G,i)),k) = Col (G,k) & k in Seg (width (DelCol (G,i))) & k in Seg (width G) ) by A2, A4, A6, A9, A13, A12, A11, A8, FINSEQ_1:1, FINSEQ_1:14; :: thesis: verum