let D be non empty set ; :: thesis: for G being Matrix of D
for i, n, m being Nat st i in Seg (width G) & width G > 1 & n in dom G & m in Seg (width (DelCol (G,i))) holds
(DelCol (G,i)) * (n,m) = (Del ((Line (G,n)),i)) . m
let G be Matrix of D; :: thesis: for i, n, m being Nat st i in Seg (width G) & width G > 1 & n in dom G & m in Seg (width (DelCol (G,i))) holds
(DelCol (G,i)) * (n,m) = (Del ((Line (G,n)),i)) . m
let i, n, m be Nat; :: thesis: ( i in Seg (width G) & width G > 1 & n in dom G & m in Seg (width (DelCol (G,i))) implies (DelCol (G,i)) * (n,m) = (Del ((Line (G,n)),i)) . m )
assume that
A1: ( i in Seg (width G) & width G > 1 & n in dom G ) and
A2: m in Seg (width (DelCol (G,i))) ; :: thesis: (DelCol (G,i)) * (n,m) = (Del ((Line (G,n)),i)) . m
thus (DelCol (G,i)) * (n,m) = (Line ((DelCol (G,i)),n)) . m by A2, Def7
.= (Del ((Line (G,n)),i)) . m by A1, Th62 ; :: thesis: verum