let I be non empty finite set ; :: thesis: 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 ()
for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b1 is Segre-Coset of A & product b2 is Segre-Coset of A & indx b1 = indx b2 holds
canonical_embedding (f,b1) = canonical_embedding (f,b2)

let A be PLS-yielding ManySortedSet of I; :: thesis: ( ( for i being Element of I holds A . i is strongly_connected ) implies for f being Collineation of ()
for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b1 is Segre-Coset of A & product b2 is Segre-Coset of A & indx b1 = indx b2 holds
canonical_embedding (f,b1) = canonical_embedding (f,b2) )

assume A1: for i being Element of I holds A . i is strongly_connected ; :: thesis: for f being Collineation of ()
for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b1 is Segre-Coset of A & product b2 is Segre-Coset of A & indx b1 = indx b2 holds
canonical_embedding (f,b1) = canonical_embedding (f,b2)

A2: now :: thesis: for o being Element of I holds A . o is connected
let o be Element of I; :: thesis: A . o is connected
A . o is strongly_connected by A1;
hence A . o is connected by Th4; :: thesis: verum
end;
let f be Collineation of (); :: thesis: for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b1 is Segre-Coset of A & product b2 is Segre-Coset of A & indx b1 = indx b2 holds
canonical_embedding (f,b1) = canonical_embedding (f,b2)

let b1, b2 be non trivial-yielding Segre-like ManySortedSubset of Carrier A; :: thesis: ( product b1 is Segre-Coset of A & product b2 is Segre-Coset of A & indx b1 = indx b2 implies canonical_embedding (f,b1) = canonical_embedding (f,b2) )
assume that
A3: ( product b1 is Segre-Coset of A & product b2 is Segre-Coset of A ) and
A4: indx b1 = indx b2 ; :: thesis: canonical_embedding (f,b1) = canonical_embedding (f,b2)
reconsider B1 = product b1, B2 = product b2 as Segre-Coset of A by A3;
per cases ( B1 misses B2 or B1 meets B2 ) ;
suppose B1 misses B2 ; :: thesis: canonical_embedding (f,b1) = canonical_embedding (f,b2)
then consider D being FinSequence of bool the carrier of () such that
A5: D . 1 = B1 and
A6: D . (len D) = B2 and
A7: for i being Nat st i in dom D holds
D . i is Segre-Coset of A and
A8: 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, A4, Th23;
defpred S1[ Nat] means ( \$1 in dom D implies for D1 being Segre-Coset of A st D1 = D . \$1 holds
for d1 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st D1 = product d1 holds
canonical_embedding (f,b1) = canonical_embedding (f,d1) );
A9: now :: thesis: for k being Nat st S1[k] holds
S1[k + 1]
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A10: S1[k] ; :: thesis: S1[k + 1]
thus S1[k + 1] :: thesis: verum
proof
assume k + 1 in dom D ; :: thesis: for D1 being Segre-Coset of A st D1 = D . (k + 1) holds
for d1 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st D1 = product d1 holds
canonical_embedding (f,b1) = canonical_embedding (f,d1)

then k + 1 <= len D by FINSEQ_3:25;
then A11: k < len D by NAT_1:13;
let D2 be Segre-Coset of A; :: thesis: ( D2 = D . (k + 1) implies for d1 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st D2 = product d1 holds
canonical_embedding (f,b1) = canonical_embedding (f,d1) )

assume A12: D2 = D . (k + 1) ; :: thesis: for d1 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st D2 = product d1 holds
canonical_embedding (f,b1) = canonical_embedding (f,d1)

let d2 be non trivial-yielding Segre-like ManySortedSubset of Carrier A; :: thesis: ( D2 = product d2 implies canonical_embedding (f,b1) = canonical_embedding (f,d2) )
assume A13: D2 = product d2 ; :: thesis: canonical_embedding (f,b1) = canonical_embedding (f,d2)
end;
end;
A16: S1[ 0 ] by FINSEQ_3:24;
for n being Nat holds S1[n] from NAT_1:sch 2(A16, A9);
then A17: S1[ len D] ;
1 in dom D by ;
then 1 <= len D by FINSEQ_3:25;
hence canonical_embedding (f,b1) = canonical_embedding (f,b2) by ; :: thesis: verum
end;
suppose B1 meets B2 ; :: thesis: canonical_embedding (f,b1) = canonical_embedding (f,b2)
end;
end;