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