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

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 A1, FINSEQ_3:99;
A4: rng (Sgm P) = P by A1, FINSEQ_1:def 13;
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_1:27;
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_1:25, ZFMISC_1:119;
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 A1, FINSEQ_3:45, MATRIX_1:25;
then A8: ( i in dom (Sgm P) & j in dom (Sgm P) ) by A2, A5, ZFMISC_1:106;
( 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 8, MATRIX_1:def 12;
hence (1. K,(card P)) * i,j = (Segm (1. K,n),P,P) * i,j by A7, A6, MATRIX_1:def 12; :: thesis: verum

end;

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