let n, i, j be Nat; :: thesis: for K being Field
for a being Element of K
for A being Matrix of n,K st i in Seg n & j in Seg n holds
Delete (a * A),i,j = a * (Delete A,i,j)
let K be Field; :: thesis: for a being Element of K
for A being Matrix of n,K st i in Seg n & j in Seg n holds
Delete (a * A),i,j = a * (Delete A,i,j)
let a be Element of K; :: thesis: for A being Matrix of n,K st i in Seg n & j in Seg n holds
Delete (a * A),i,j = a * (Delete A,i,j)
let A be Matrix of n,K; :: thesis: ( i in Seg n & j in Seg n implies Delete (a * A),i,j = a * (Delete A,i,j) )
assume A1: ( i in Seg n & j in Seg n ) ; :: thesis: Delete (a * A),i,j = a * (Delete A,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 * A),i,j = Deleting (a * A),i,j by A1, LAPLACE:def 1
.= Segm (a * A),((Seg n) \ {i}),((Seg n) \ {j}) by MATRIX13:58
.= a * (Segm A,((Seg n) \ {i}),((Seg n) \ {j})) by A2, A3, MATRIX13:63
.= a * (Deleting A,i,j) by MATRIX13:58
.= a * (Delete A,i,j) by A1, LAPLACE:def 1 ; :: thesis: verum