let D be non empty set ; 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 V3()
let G be Matrix of D; for i being Nat st width G > 1 & i in Seg (width G) holds
not DelCol (G,i) is V3()
let i be Nat; ( width G > 1 & i in Seg (width G) implies not DelCol (G,i) is V3() )
assume that
A1:
width G > 1
and
A2:
i in Seg (width G)
; DelCol (G,i) is V3()
(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 V3()
by A3; verum