let D be non empty set ; for G being Matrix of D
for i, k being Nat st k in dom G holds
Line ((DelCol (G,i)),k) = Del ((Line (G,k)),i)
let G be Matrix of D; for i, k being Nat st k in dom G holds
Line ((DelCol (G,i)),k) = Del ((Line (G,k)),i)
let i, k be Nat; ( k in dom G implies Line ((DelCol (G,i)),k) = Del ((Line (G,k)),i) )
set D = DelCol (G,i);
assume A1:
k in dom G
; Line ((DelCol (G,i)),k) = Del ((Line (G,k)),i)
len (DelCol (G,i)) = len G
by Def13;
then A2:
dom (DelCol (G,i)) = dom G
by FINSEQ_3:29;
(DelCol (G,i)) . k = Del ((Line (G,k)),i)
by A1, Def13;
hence
Line ((DelCol (G,i)),k) = Del ((Line (G,k)),i)
by A1, A2, Th60; verum