begin
theorem Th1:
theorem Th2:
theorem Th3:
theorem Th4:
theorem
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
:: deftheorem defines diff PENCIL_3:def 1 :
theorem Th19:
begin
:: deftheorem Def2 defines '||' PENCIL_3:def 2 :
theorem Th20:
theorem Th21:
theorem Th22:
theorem Th23:
theorem Th24:
theorem Th25:
definition
let I be non
empty finite set ;
let A be
PLS-yielding ManySortedSet of
I;
assume A1:
for
i being
Element of
I holds
A . i is
strongly_connected
;
let f be
Collineation of
Segre_Product A;
func permutation_of_indices f -> Permutation of
I means :
Def3:
for
i,
j being
Element of
I holds
(
it . i = j iff for
B1 being
Segre-Coset of
A for
b1,
b2 being non
trivial-yielding Segre-like ManySortedSubset of
Carrier A st
B1 = product b1 &
f .: B1 = product b2 &
indx b1 = i holds
indx b2 = j );
existence
ex b1 being Permutation of I st
for i, j being Element of I holds
( b1 . i = j iff for B1 being Segre-Coset of A
for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & f .: B1 = product b2 & indx b1 = i holds
indx b2 = j )
by A1, Th25;
uniqueness
for b1, b2 being Permutation of I st ( for i, j being Element of I holds
( b1 . i = j iff for B1 being Segre-Coset of A
for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & f .: B1 = product b2 & indx b1 = i holds
indx b2 = j ) ) & ( for i, j being Element of I holds
( b2 . i = j iff for B1 being Segre-Coset of A
for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & f .: B1 = product b2 & indx b1 = i holds
indx b2 = j ) ) holds
b1 = b2
end;
:: deftheorem Def3 defines permutation_of_indices PENCIL_3:def 3 :
begin
:: deftheorem Def4 defines canonical_embedding PENCIL_3:def 4 :
theorem Th26:
theorem Th27:
:: deftheorem Def5 defines canonical_embedding PENCIL_3:def 5 :
theorem