let D be non empty set ; :: thesis: for G being Matrix of D
for i, m being Nat st i in Seg (width G) & width G = m + 1 holds
width (DelCol (G,i)) = m
let G be Matrix of D; :: thesis: for i, m being Nat st i in Seg (width G) & width G = m + 1 holds
width (DelCol (G,i)) = m
let i, m be Nat; :: thesis: ( i in Seg (width G) & width G = m + 1 implies width (DelCol (G,i)) = m )
set D = DelCol (G,i);
assume that
A1: i in Seg (width G) and
A2: width G = m + 1 ; :: thesis: width (DelCol (G,i)) = m
width G <> 0 by A2;
then 0 < len G by Def3;
then 0 + 1 <= len G by NAT_1:13;
then 1 in dom G by FINSEQ_3:25;
then A3: Line ((DelCol (G,i)),1) = Del ((Line (G,1)),i) by Th62;
A4: ( dom (Line (G,1)) = Seg (len (Line (G,1))) & len (Line ((DelCol (G,i)),1)) = width (DelCol (G,i)) ) by Def7, FINSEQ_1:def 3;
len (Line (G,1)) = m + 1 by A2, Def7;
hence width (DelCol (G,i)) = m by A1, A2, A3, A4, FINSEQ_3:109; :: thesis: verum