let D be non empty set ; :: thesis: for G being Matrix of D
for k, n, m being Nat st width G = m + 1 & m > 0 & k in Seg m & n in dom G holds
( k in Seg (width G) & (DelCol (G,(width G))) * (n,k) = G * (n,k) & width G in Seg (width G) )
let G be Matrix of D; :: thesis: for k, n, m being Nat st width G = m + 1 & m > 0 & k in Seg m & n in dom G holds
( k in Seg (width G) & (DelCol (G,(width G))) * (n,k) = G * (n,k) & width G in Seg (width G) )
let k, n, m be Nat; :: thesis: ( width G = m + 1 & m > 0 & k in Seg m & n in dom G implies ( k in Seg (width G) & (DelCol (G,(width G))) * (n,k) = G * (n,k) & width G in Seg (width G) ) )
assume that
A1: width G = m + 1 and
A2: m > 0 and
A3: k in Seg m and
A4: n in dom G ; :: thesis: ( k in Seg (width G) & (DelCol (G,(width G))) * (n,k) = G * (n,k) & width G in Seg (width G) )
k <= m by A3, FINSEQ_1:1;
then A5: k < width G by A1, NAT_1:13;
1 <= width G by A1, A2, SEQM_3:43;
then A6: width G in Seg (width G) by FINSEQ_1:1;
1 <= k by A3, FINSEQ_1:1;
hence ( k in Seg (width G) & (DelCol (G,(width G))) * (n,k) = G * (n,k) & width G in Seg (width G) ) by A1, A2, A4, A6, A5, Th69; :: thesis: verum