let M1, M2 be Matrix of K; :: thesis: ( 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
A25: len M1 = len M and
A26: for k being Nat st k in dom M holds
M1 . k = Del ((Line (M,k)),i) and
A27: len M2 = len M and
A28: for k being Nat st k in dom M holds
M2 . k = Del ((Line (M,k)),i) ; :: thesis: M1 = M2
A29: dom M1 = dom M by A25, FINSEQ_3:29;

now

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

end;

hence M1 = M2 by A25, A27, FINSEQ_2:9; :: thesis: verum