let M1, M2 be Matrix of D; :: thesis:
assume that
A24: len M1 = len M and
A25: for k being Nat st k in dom M holds
M1 . k = Del ((Line (M,k)),i) and
A26: len M2 = len M and
A27: for k being Nat st k in dom M holds
M2 . k = Del ((Line (M,k)),i) ; :: thesis:
A28: dom M1 = dom M by A24, FINSEQ_3:29;

let k be Nat; :: thesis:
assume A29: k in dom M1 ; :: thesis:
hence M1 . k = Del ((Line (M,k)),i) by A25, A28
.= M2 . k by A27, A28, A29 ;
:: thesis:

end;