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 & 1 <= k & k < i holds
( Col ((DelCol (G,i)),k) = Col (G,k) & k in Seg (width (DelCol (G,i))) & k 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 & 1 <= k & k < i holds
( Col ((DelCol (G,i)),k) = Col (G,k) & k in Seg (width (DelCol (G,i))) & k in Seg (width G) )
let i, k, m be Nat; ( i in Seg (width G) & width G = m + 1 & m > 0 & 1 <= k & k < i implies ( Col ((DelCol (G,i)),k) = Col (G,k) & k in Seg (width (DelCol (G,i))) & k 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:
1 <= k
and
A5:
k < i
; ( Col ((DelCol (G,i)),k) = Col (G,k) & k in Seg (width (DelCol (G,i))) & k in Seg (width G) )
A6:
width (DelCol (G,i)) = m
by A1, A2, Th63;
A7:
1 < width G
by A2, A3, SEQM_3:43;
A8:
len (DelCol (G,i)) = len G
by Def13;
i <= m + 1
by A1, A2, FINSEQ_1:1;
then A9:
k < m + 1
by A5, XXREAL_0:2;
then A10:
k in Seg (width G)
by A2, A4, FINSEQ_1:1;
A11:
len (Col (G,k)) = len G
by Def8;
A12:
len (Col ((DelCol (G,i)),k)) = len (DelCol (G,i))
by Def8;
A13:
k <= m
by A9, NAT_1:13;
then A14:
k in Seg (width (DelCol (G,i)))
by A4, A6, 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)) . jlet j be
Nat;
( 1 <= j & j <= len (Col ((DelCol (G,i)),k)) implies (Col ((DelCol (G,i)),k)) . j = (Col (G,k)) . j )A15:
(
dom (DelCol (G,i)) = Seg (len (DelCol (G,i))) &
dom G = Seg (len G) )
by FINSEQ_1:def 3;
assume
( 1
<= j &
j <= len (Col ((DelCol (G,i)),k)) )
;
(Col ((DelCol (G,i)),k)) . j = (Col (G,k)) . jthen A16:
j in dom (DelCol (G,i))
by A12, 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, A16, A15, Th66
.=
(Line (G,j)) . k
by A5, FINSEQ_3:110
.=
(Col (G,k)) . j
by A10, A8, A16, A15, Th42
;
verum end;
hence
( Col ((DelCol (G,i)),k) = Col (G,k) & k in Seg (width (DelCol (G,i))) & k in Seg (width G) )
by A2, A4, A6, A9, A13, A12, A11, A8, FINSEQ_1:1, FINSEQ_1:14; verum