let n, i, j 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:119;
A3: Indices A = [:(Seg n),(Seg n):] by MATRIX_1:25;
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