let D be non empty set ; for G being Matrix of D
for i, k, m being Nat st i in Seg (width G) & width G = m + 1 & m > 0 & i <= k & k <= m holds
( Col ((DelCol (G,i)),k) = Col (G,(k + 1)) & k in Seg (width (DelCol (G,i))) & k + 1 in Seg (width G) )
let G be Matrix of D; for i, k, m being Nat st i in Seg (width G) & width G = m + 1 & m > 0 & i <= k & k <= m holds
( Col ((DelCol (G,i)),k) = Col (G,(k + 1)) & k in Seg (width (DelCol (G,i))) & k + 1 in Seg (width G) )
let i, k, m be Nat; ( i in Seg (width G) & width G = m + 1 & m > 0 & i <= k & k <= m implies ( Col ((DelCol (G,i)),k) = Col (G,(k + 1)) & k in Seg (width (DelCol (G,i))) & k + 1 in Seg (width G) ) )
set N = DelCol (G,i);
assume that
A1:
i in Seg (width G)
and
A2:
width G = m + 1
and
A3:
m > 0
and
A4:
i <= k
and
A5:
k <= m
; ( Col ((DelCol (G,i)),k) = Col (G,(k + 1)) & k in Seg (width (DelCol (G,i))) & k + 1 in Seg (width G) )
A6:
len (Col ((DelCol (G,i)),k)) = len (DelCol (G,i))
by Def8;
A7:
1 < width G
by A2, A3, SEQM_3:43;
A8:
len (DelCol (G,i)) = len G
by Def13;
A9:
( 1 <= k + 1 & k + 1 <= m + 1 )
by A5, NAT_1:11, XREAL_1:6;
then A10:
k + 1 in Seg (width G)
by A2, FINSEQ_1:1;
1 <= i
by A1, FINSEQ_1:1;
then A11:
1 <= k
by A4, XXREAL_0:2;
A12:
len (Col (G,(k + 1))) = len G
by Def8;
A13:
width (DelCol (G,i)) = m
by A1, A2, Th63;
then A14:
k in Seg (width (DelCol (G,i)))
by A5, A11, FINSEQ_1:1;
now for j being Nat st 1 <= j & j <= len (Col ((DelCol (G,i)),k)) holds
(Col ((DelCol (G,i)),k)) . j = (Col (G,(k + 1))) . jlet j be
Nat;
( 1 <= j & j <= len (Col ((DelCol (G,i)),k)) implies (Col ((DelCol (G,i)),k)) . j = (Col (G,(k + 1))) . j )A15:
(
dom (DelCol (G,i)) = Seg (len (DelCol (G,i))) &
dom G = Seg (len G) )
by FINSEQ_1:def 3;
A16:
(
len (Line (G,j)) = m + 1 &
dom (Line (G,j)) = Seg (len (Line (G,j))) )
by A2, Def7, FINSEQ_1:def 3;
assume
( 1
<= j &
j <= len (Col ((DelCol (G,i)),k)) )
;
(Col ((DelCol (G,i)),k)) . j = (Col (G,(k + 1))) . jthen A17:
j in dom (DelCol (G,i))
by A6, FINSEQ_3:25;
hence (Col ((DelCol (G,i)),k)) . j =
(DelCol (G,i)) * (
j,
k)
by Def8
.=
(Del ((Line (G,j)),i)) . k
by A1, A14, A7, A8, A17, A15, Th66
.=
(Line (G,j)) . (k + 1)
by A1, A2, A4, A5, A16, FINSEQ_3:111
.=
(Col (G,(k + 1))) . j
by A10, A8, A17, A15, Th42
;
verum end;
hence
( Col ((DelCol (G,i)),k) = Col (G,(k + 1)) & k in Seg (width (DelCol (G,i))) & k + 1 in Seg (width G) )
by A2, A5, A13, A9, A11, A6, A12, A8, FINSEQ_1:1, FINSEQ_1:14; verum