let M1, M2 be Matrix of D; ( len M1 = len M & ( for k being Nat st k in dom M holds
M1 . k = Del ((Line (M,k)),i) ) & len M2 = len M & ( for k being Nat st k in dom M holds
M2 . k = Del ((Line (M,k)),i) ) implies M1 = M2 )
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)
; M1 = M2
A28:
dom M1 = dom M
by A24, FINSEQ_3:29;
hence
M1 = M2
by A24, A26, FINSEQ_2:9; verum