let D be non empty set ; :: thesis: for G being Matrix of D
for i being Nat st i in Seg (width G) & width G > 0 holds
width G = (width (DelCol (G,i))) + 1
let G be Matrix of D; :: thesis: for i being Nat st i in Seg (width G) & width G > 0 holds
width G = (width (DelCol (G,i))) + 1
let i be Nat; :: thesis: ( i in Seg (width G) & width G > 0 implies width G = (width (DelCol (G,i))) + 1 )
assume that
A1: i in Seg (width G) and
A2: width G > 0 ; :: thesis: width G = (width (DelCol (G,i))) + 1
ex m being Nat st width G = m + 1 by A2, NAT_1:6;
hence width G = (width (DelCol (G,i))) + 1 by A1, Th63; :: thesis: verum