let D be non empty set ; :: thesis: for G being Matrix of D
for i, k, n, m being Nat st i in Seg (width G) & width G = m + 1 & m > 0 & n in dom G & 1 <= k & k < i holds
( (DelCol (G,i)) * (n,k) = G * (n,k) & k in Seg (width G) )
let G be Matrix of D; :: thesis: for i, k, n, m being Nat st i in Seg (width G) & width G = m + 1 & m > 0 & n in dom G & 1 <= k & k < i holds
( (DelCol (G,i)) * (n,k) = G * (n,k) & k in Seg (width G) )
let i, k, n, m be Nat; :: thesis: ( i in Seg (width G) & width G = m + 1 & m > 0 & n in dom G & 1 <= k & k < i implies ( (DelCol (G,i)) * (n,k) = G * (n,k) & k in Seg (width G) ) )
assume that
A1: i in Seg (width G) and
A2: ( width G = m + 1 & m > 0 ) and
A3: n in dom G and
A4: ( 1 <= k & k < i ) ; :: thesis: ( (DelCol (G,i)) * (n,k) = G * (n,k) & k in Seg (width G) )
A5: len (DelCol (G,i)) = len G by Def13;
A6: ( dom G = Seg (len G) & Seg (len (DelCol (G,i))) = dom (DelCol (G,i)) ) by FINSEQ_1:def 3;
Col ((DelCol (G,i)),k) = Col (G,k) by A1, A2, A4, Th67;
hence (DelCol (G,i)) * (n,k) = (Col (G,k)) . n by A3, A6, A5, Def8
.= G * (n,k) by A3, Def8 ;
:: thesis: k in Seg (width G)
thus k in Seg (width G) by A1, A2, A4, Th67; :: thesis: verum