let D be non empty set ; for G being Matrix of D
for i, k, n, m being Nat st i in Seg (width G) & width G = m + 1 & m > 0 & n in dom G & 1 <= k & k < i holds
( (DelCol (G,i)) * (n,k) = G * (n,k) & k in Seg (width G) )
let G be Matrix of D; for i, k, n, m being Nat st i in Seg (width G) & width G = m + 1 & m > 0 & n in dom G & 1 <= k & k < i holds
( (DelCol (G,i)) * (n,k) = G * (n,k) & k in Seg (width G) )
let i, k, n, m be Nat; ( i in Seg (width G) & width G = m + 1 & m > 0 & n in dom G & 1 <= k & k < i implies ( (DelCol (G,i)) * (n,k) = G * (n,k) & k in Seg (width G) ) )
assume that
A1:
i in Seg (width G)
and
A2:
( width G = m + 1 & m > 0 )
and
A3:
n in dom G
and
A4:
( 1 <= k & k < i )
; ( (DelCol (G,i)) * (n,k) = G * (n,k) & k in Seg (width G) )
A5:
len (DelCol (G,i)) = len G
by Def13;
A6:
( dom G = Seg (len G) & Seg (len (DelCol (G,i))) = dom (DelCol (G,i)) )
by FINSEQ_1:def 3;
Col ((DelCol (G,i)),k) = Col (G,k)
by A1, A2, A4, Th67;
hence (DelCol (G,i)) * (n,k) =
(Col (G,k)) . n
by A3, A6, A5, Def8
.=
G * (n,k)
by A3, Def8
;
k in Seg (width G)
thus
k in Seg (width G)
by A1, A2, A4, Th67; verum