let i be Nat; for K being Field
for M being Matrix of K holds Segm (M,(Seg (len M)),((Seg (width M)) \ {i})) = DelCol (M,i)
let K be Field; for M being Matrix of K holds Segm (M,(Seg (len M)),((Seg (width M)) \ {i})) = DelCol (M,i)
let M be Matrix of K; Segm (M,(Seg (len M)),((Seg (width M)) \ {i})) = DelCol (M,i)
set SW = Seg (width M);
set Si = (Seg (width M)) \ {i};
set SL = Seg (len M);
set SEGM = Segm (M,(Seg (len M)),((Seg (width M)) \ {i}));
set D = DelCol (M,i);
card (Seg (len M)) = len M
by FINSEQ_1:57;
then A1:
len (Segm (M,(Seg (len M)),((Seg (width M)) \ {i}))) = len M
by MATRIX_0:def 2;
A2:
now for j being Nat st 1 <= j & j <= len M holds
(Segm (M,(Seg (len M)),((Seg (width M)) \ {i}))) . j = (DelCol (M,i)) . jlet j be
Nat;
( 1 <= j & j <= len M implies (Segm (M,(Seg (len M)),((Seg (width M)) \ {i}))) . j = (DelCol (M,i)) . j )assume that A3:
1
<= j
and A4:
j <= len M
;
(Segm (M,(Seg (len M)),((Seg (width M)) \ {i}))) . j = (DelCol (M,i)) . jA5:
j in Seg (len M)
by A3, A4;
then A6:
j in dom M
by FINSEQ_1:def 3;
Sgm (Seg (len M)) = idseq (len M)
by FINSEQ_3:48;
then A7:
(Sgm (Seg (len M))) . j = j
by A5, FINSEQ_2:49;
len (Line (M,j)) = width M
by MATRIX_0:def 7;
then A8:
dom (Line (M,j)) = Seg (width M)
by FINSEQ_1:def 3;
A9:
card (Seg (len M)) = len M
by FINSEQ_1:57;
then A10:
Line (
(Segm (M,(Seg (len M)),((Seg (width M)) \ {i}))),
j)
= (Segm (M,(Seg (len M)),((Seg (width M)) \ {i}))) . j
by A5, MATRIX_0:52;
Line (
(Segm (M,(Seg (len M)),((Seg (width M)) \ {i}))),
j)
= (Line (M,((Sgm (Seg (len M))) . j))) * (Sgm ((Seg (width M)) \ {i}))
by A9, A5, Th47, XBOOLE_1:36;
then
(Segm (M,(Seg (len M)),((Seg (width M)) \ {i}))) . j = Del (
(Line (M,j)),
i)
by A7, A10, A8, FINSEQ_3:def 2;
hence
(Segm (M,(Seg (len M)),((Seg (width M)) \ {i}))) . j = (DelCol (M,i)) . j
by A6, MATRIX_0:def 13;
verum end;
len (DelCol (M,i)) = len M
by MATRIX_0:def 13;
hence
Segm (M,(Seg (len M)),((Seg (width M)) \ {i})) = DelCol (M,i)
by A1, A2; verum