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 & i <= k & k <= m holds
( (DelCol (G,i)) * (n,k) = G * (n,(k + 1)) & k + 1 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 & i <= k & k <= m holds
( (DelCol (G,i)) * (n,k) = G * (n,(k + 1)) & k + 1 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 & i <= k & k <= m implies ( (DelCol (G,i)) * (n,k) = G * (n,(k + 1)) & k + 1 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: ( i <= k & k <= m ) ; :: thesis: ( (DelCol (G,i)) * (n,k) = G * (n,(k + 1)) & k + 1 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 + 1)) by A1, A2, A4, Th68;
hence (DelCol (G,i)) * (n,k) = (Col (G,(k + 1))) . n by A3, A6, A5, Def8
.= G * (n,(k + 1)) by A3, Def8 ;
:: thesis: k + 1 in Seg (width G)
thus k + 1 in Seg (width G) by A1, A2, A4, Th68; :: thesis: verum