let n be Nat; :: thesis: for K being Field
for P being finite without_zero Subset of NAT st P c= Seg n holds
Segm ((1. (K,n)),P,P) = 1. (K,(card P))
let K be Field; :: thesis: for P being finite without_zero Subset of NAT st P c= Seg n holds
Segm ((1. (K,n)),P,P) = 1. (K,(card P))
let P be finite without_zero Subset of NAT; :: thesis: ( P c= Seg n implies Segm ((1. (K,n)),P,P) = 1. (K,(card P)) )
assume A1: P c= Seg n ; :: thesis: Segm ((1. (K,n)),P,P) = 1. (K,(card P))
set S = Segm ((1. (K,n)),P,P);

now :: thesis: for i, j being Nat st [i,j] in Indices (1. (K,(card P))) holds
(1. (K,(card P))) * (i,j) = (Segm ((1. (K,n)),P,P)) * (i,j)

set SP = Sgm P;
let i, j be Nat; :: thesis: ( [i,j] in Indices (1. (K,(card P))) implies (1. (K,(card P))) * (i,j) = (Segm ((1. (K,n)),P,P)) * (i,j) )
assume A2: [i,j] in Indices (1. (K,(card P))) ; :: thesis: (1. (K,(card P))) * (i,j) = (Segm ((1. (K,n)),P,P)) * (i,j)
A3: Sgm P is one-to-one by FINSEQ_3:92;
A4: rng (Sgm P) = P by FINSEQ_1:def 14;
reconsider Spi = (Sgm P) . i, Spj = (Sgm P) . j as Nat by VALUED_0:12;
A5: Indices (1. (K,(card P))) = Indices (Segm ((1. (K,n)),P,P)) by MATRIX_0:26;
then A6: (Segm ((1. (K,n)),P,P)) * (i,j) = (1. (K,n)) * (Spi,Spj) by A2, MATRIX13:def 1;
( Indices (1. (K,n)) = [:(Seg n),(Seg n):] & [:P,P:] c= [:(Seg n),(Seg n):] ) by A1, MATRIX_0:24, ZFMISC_1:96;
then A7: [((Sgm P) . i),((Sgm P) . j)] in Indices (1. (K,n)) by A2, A5, A4, MATRIX13:17;
( Indices (Segm ((1. (K,n)),P,P)) = [:(Seg (card P)),(Seg (card P)):] & dom (Sgm P) = Seg (card P) ) by FINSEQ_3:40, MATRIX_0:24;
then A8: ( i in dom (Sgm P) & j in dom (Sgm P) ) by A2, A5, ZFMISC_1:87;
( i = j or i <> j ) ;
then ( ( (Segm ((1. (K,n)),P,P)) * (i,j) = 1_ K & (1. (K,(card P))) * (i,j) = 1_ K ) or ( (1. (K,(card P))) * (i,j) = 0. K & (Sgm P) . i <> (Sgm P) . j ) ) by A2, A3, A7, A8, A6, FUNCT_1:def 4, MATRIX_1:def 3;
hence (1. (K,(card P))) * (i,j) = (Segm ((1. (K,n)),P,P)) * (i,j) by A7, A6, MATRIX_1:def 3; :: thesis: verum

end;

hence Segm ((1. (K,n)),P,P) = 1. (K,(card P)) by MATRIX_0:27; :: thesis: verum