let I be non empty finite set ; for A being PLS-yielding ManySortedSet of I st ( for i being Element of I holds A . i is strongly_connected ) holds
for f being Collineation of (Segre_Product A)
for B1, B2 being Segre-Coset of A
for b1, b2, b3, b4 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & B2 = product b2 & f .: B1 = product b3 & f .: B2 = product b4 & indx b1 = indx b2 holds
indx b3 = indx b4
let A be PLS-yielding ManySortedSet of I; ( ( for i being Element of I holds A . i is strongly_connected ) implies for f being Collineation of (Segre_Product A)
for B1, B2 being Segre-Coset of A
for b1, b2, b3, b4 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & B2 = product b2 & f .: B1 = product b3 & f .: B2 = product b4 & indx b1 = indx b2 holds
indx b3 = indx b4 )
assume A1:
for i being Element of I holds A . i is strongly_connected
; for f being Collineation of (Segre_Product A)
for B1, B2 being Segre-Coset of A
for b1, b2, b3, b4 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & B2 = product b2 & f .: B1 = product b3 & f .: B2 = product b4 & indx b1 = indx b2 holds
indx b3 = indx b4
let f be Collineation of (Segre_Product A); for B1, B2 being Segre-Coset of A
for b1, b2, b3, b4 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & B2 = product b2 & f .: B1 = product b3 & f .: B2 = product b4 & indx b1 = indx b2 holds
indx b3 = indx b4
let B1, B2 be Segre-Coset of A; for b1, b2, b3, b4 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & B2 = product b2 & f .: B1 = product b3 & f .: B2 = product b4 & indx b1 = indx b2 holds
indx b3 = indx b4
let b1, b2, b3, b4 be non trivial-yielding Segre-like ManySortedSubset of Carrier A; ( B1 = product b1 & B2 = product b2 & f .: B1 = product b3 & f .: B2 = product b4 & indx b1 = indx b2 implies indx b3 = indx b4 )
assume that
A3:
B1 = product b1
and
A4:
B2 = product b2
and
A5:
( f .: B1 = product b3 & f .: B2 = product b4 )
; ( not indx b1 = indx b2 or indx b3 = indx b4 )
assume A6:
indx b1 = indx b2
; indx b3 = indx b4
per cases
( B1 misses B2 or B1 meets B2 )
;
suppose A7:
B1 misses B2
;
indx b3 = indx b4reconsider fB1 =
f .: B1,
fB2 =
f .: B2 as
Segre-Coset of
A by A1, PENCIL_2:24;
f is
bijective Function of the
carrier of
(Segre_Product A), the
carrier of
(Segre_Product A)
by PENCIL_2:def 4;
then A8:
fB1 misses fB2
by A7, FUNCT_1:66;
consider D being
FinSequence of
bool the
carrier of
(Segre_Product A) such that A9:
D . 1
= B1
and A10:
D . (len D) = B2
and A11:
for
i being
Nat st
i in dom D holds
D . i is
Segre-Coset of
A
and A12:
for
i being
Nat st 1
<= i &
i < len D holds
for
Di,
Di1 being
Segre-Coset of
A st
Di = D . i &
Di1 = D . (i + 1) holds
(
Di misses Di1 &
Di '||' Di1 )
by A2, A3, A4, A6, A7, Th23;
deffunc H1(
Nat)
-> Element of
bool the
carrier of
(Segre_Product A) =
f .: (D . $1);
consider E being
FinSequence of
bool the
carrier of
(Segre_Product A) such that A13:
(
len E = len D & ( for
j being
Nat st
j in dom E holds
E . j = H1(
j) ) )
from FINSEQ_2:sch 1();
A14:
dom E = Seg (len D)
by A13, FINSEQ_1:def 3;
A15:
for
i being
Nat st 1
<= i &
i < len E holds
for
Ei,
Ei1 being
Segre-Coset of
A st
Ei = E . i &
Ei1 = E . (i + 1) holds
(
Ei misses Ei1 &
Ei '||' Ei1 )
proof
let i be
Nat;
( 1 <= i & i < len E implies for Ei, Ei1 being Segre-Coset of A st Ei = E . i & Ei1 = E . (i + 1) holds
( Ei misses Ei1 & Ei '||' Ei1 ) )
A16:
f is
bijective Function of the
carrier of
(Segre_Product A), the
carrier of
(Segre_Product A)
by PENCIL_2:def 4;
assume A17:
( 1
<= i &
i < len E )
;
for Ei, Ei1 being Segre-Coset of A st Ei = E . i & Ei1 = E . (i + 1) holds
( Ei misses Ei1 & Ei '||' Ei1 )
then
i in dom D
by A13, FINSEQ_3:25;
then reconsider Di =
D . i as
Segre-Coset of
A by A11;
( 1
<= i + 1 &
i + 1
<= len E )
by A17, NAT_1:13;
then
i + 1
in dom D
by A13, FINSEQ_3:25;
then reconsider Di1 =
D . (i + 1) as
Segre-Coset of
A by A11;
let Ei,
Ei1 be
Segre-Coset of
A;
( Ei = E . i & Ei1 = E . (i + 1) implies ( Ei misses Ei1 & Ei '||' Ei1 ) )
assume that A18:
Ei = E . i
and A19:
Ei1 = E . (i + 1)
;
( Ei misses Ei1 & Ei '||' Ei1 )
i in Seg (len D)
by A13, A17, FINSEQ_1:1;
then A20:
Ei = f .: (D . i)
by A13, A14, A18;
( 1
<= i + 1 &
i + 1
<= len E )
by A17, NAT_1:13;
then
i + 1
in Seg (len D)
by A13, FINSEQ_1:1;
then A21:
Ei1 = f .: (D . (i + 1))
by A13, A14, A19;
Di misses Di1
by A12, A13, A17;
hence
Ei misses Ei1
by A20, A21, A16, FUNCT_1:66;
Ei '||' Ei1
Di '||' Di1
by A12, A13, A17;
hence
Ei '||' Ei1
by A20, A21, Th20;
verum
end; A22:
for
i being
Nat st
i in dom E holds
E . i is
Segre-Coset of
A
len E in dom D
by A4, A10, A13, FUNCT_1:def 2;
then
len E in Seg (len D)
by FINSEQ_1:def 3;
then A24:
E . (len E) = f .: B2
by A10, A13, A14;
1
in dom D
by A3, A9, FUNCT_1:def 2;
then
1
in Seg (len D)
by FINSEQ_1:def 3;
then
E . 1
= f .: B1
by A9, A13, A14;
hence
indx b3 = indx b4
by A2, A5, A24, A22, A15, A8, Th23;
verum end; end;