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 FINSEQ_1:4, NAT_1:14, XREAL_1:235;
then card (Seg n) = (n -' 1) + 1 by FINSEQ_1:78;
then A2: card ((Seg n) \ {i}) = n -' 1 by A1, STIRL2_1:65;
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