let D be non empty set ; :: thesis: for G being Matrix of D
for i being Nat st width G > 1 & i in Seg (width G) holds
not DelCol (G,i) is empty-yielding
let G be Matrix of D; :: thesis: for i being Nat st width G > 1 & i in Seg (width G) holds
not DelCol (G,i) is empty-yielding
let i be Nat; :: thesis: ( width G > 1 & i in Seg (width G) implies not DelCol (G,i) is empty-yielding )
assume that
A1: width G > 1 and
A2: i in Seg (width G) ; :: thesis: DelCol (G,i) is empty-yielding
(width (DelCol (G,i))) + 1 > 0 + 1 by A1, A2, Th64;
then A3: width (DelCol (G,i)) > 0 ;
then len (DelCol (G,i)) > 0 by Def3;
hence DelCol (G,i) is empty-yielding by A3; :: thesis: verum