let i, n be Nat; for K being Field st i in Seg n holds
Delete ((1. (K,n)),i,i) = 1. (K,(n -' 1))
let K be Field; ( i in Seg n implies Delete ((1. (K,n)),i,i) = 1. (K,(n -' 1)) )
assume A1:
i in Seg n
; Delete ((1. (K,n)),i,i) = 1. (K,(n -' 1))
then
n <> 0
;
then
n >= 1
by NAT_1:14;
then
n -' 1 = n - 1
by XREAL_1:233;
then
card (Seg n) = (n -' 1) + 1
by FINSEQ_1:57;
then A2:
card ((Seg n) \ {i}) = n -' 1
by A1, STIRL2_1:55;
thus Delete ((1. (K,n)),i,i) =
Deleting ((1. (K,n)),i,i)
by A1, LAPLACE:def 1
.=
Segm ((1. (K,n)),((Seg n) \ {i}),((Seg n) \ {i}))
by MATRIX13:58
.=
1. (K,(n -' 1))
by A2, Th2, XBOOLE_1:36
; verum