let D be non empty set ; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum