let i, j, n be Nat; :: thesis: for K being Field
for A, B being Matrix of n,K st i in Seg n & j in Seg n holds
Delete ((A + B),i,j) = (Delete (A,i,j)) + (Delete (B,i,j))
let K be Field; :: thesis: for A, B being Matrix of n,K st i in Seg n & j in Seg n holds
Delete ((A + B),i,j) = (Delete (A,i,j)) + (Delete (B,i,j))
let A, B be Matrix of n,K; :: thesis: ( i in Seg n & j in Seg n implies Delete ((A + B),i,j) = (Delete (A,i,j)) + (Delete (B,i,j)) )
assume A1: ( i in Seg n & j in Seg n ) ; :: thesis: Delete ((A + B),i,j) = (Delete (A,i,j)) + (Delete (B,i,j))
( (Seg n) \ {i} c= Seg n & (Seg n) \ {j} c= Seg n ) by XBOOLE_1:36;
then A2: [:((Seg n) \ {i}),((Seg n) \ {j}):] c= [:(Seg n),(Seg n):] by ZFMISC_1:96;
A3: Indices A = [:(Seg n),(Seg n):] by MATRIX_0:24;
thus Delete ((A + B),i,j) = Deleting ((A + B),i,j) by A1, LAPLACE:def 1
.= Segm ((A + B),((Seg n) \ {i}),((Seg n) \ {j})) by MATRIX13:58
.= (Segm (A,((Seg n) \ {i}),((Seg n) \ {j}))) + (Segm (B,((Seg n) \ {i}),((Seg n) \ {j}))) by A2, A3, Th3
.= (Deleting (A,i,j)) + (Segm (B,((Seg n) \ {i}),((Seg n) \ {j}))) by MATRIX13:58
.= (Deleting (A,i,j)) + (Deleting (B,i,j)) by MATRIX13:58
.= (Delete (A,i,j)) + (Deleting (B,i,j)) by A1, LAPLACE:def 1
.= (Delete (A,i,j)) + (Delete (B,i,j)) by A1, LAPLACE:def 1 ; :: thesis: verum