let i, n be Nat; :: thesis: for K being Field st i in Seg n holds
Delete ((1. (K,n)),i,i) = 1. (K,(n -' 1))
let K be Field; :: thesis: ( i in Seg n implies Delete ((1. (K,n)),i,i) = 1. (K,(n -' 1)) )
assume A1: i in Seg n ; :: thesis: 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 ; :: thesis: verum