let I be non empty finite set ; :: thesis:
let A be PLS-yielding ManySortedSet of I; :: thesis:
assume A1: for i being Element of I holds A . i is strongly_connected ; :: thesis:

A2: now :: thesis:

let o be Element of I; :: thesis:
A . o is strongly_connected by A1;
hence A . o is connected by Th4; :: thesis:

end;

let f be Collineation of (Segre_Product A); :: thesis:
let b1, b2 be non trivial-yielding Segre-like ManySortedSubset of Carrier A; :: thesis:
assume that
A3: ( product b1 is Segre-Coset of A & product b2 is Segre-Coset of A ) and
A4: indx b1 = indx b2 ; :: thesis:
reconsider B1 = product b1, B2 = product b2 as Segre-Coset of A by A3;

per cases ;

suppose B1 misses B2 ; :: thesis:

then consider D being FinSequence of bool the carrier of (Segre_Product A) 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 S₁[ 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:

let k be Nat; :: thesis:
assume A10: S₁[k] ; :: thesis:
thus S₁[k + 1] :: thesis:

proof

assume k + 1 in dom D ; :: thesis:
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:
assume A12: D2 = D . (k + 1) ; :: thesis:
let d2 be non trivial-yielding Segre-like ManySortedSubset of Carrier A; :: thesis:
assume A13: D2 = product d2 ; :: thesis:

per cases by NAT_1:14;

suppose k = 0 ; :: thesis:

hence canonical_embedding (f,b1) = canonical_embedding (f,d2) by A5, A12, A13, PUA2MSS1:2; :: thesis:

end;

suppose A14: 1 <= k ; :: thesis:

then k in dom D by A11, FINSEQ_3:25;
then reconsider D1 = D . k as Segre-Coset of A by A7;
consider d1 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that
A15: product d1 = D1 and
d1 . (indx d1) = [#] (A . (indx d1)) by PENCIL_2:def 2;
( D1 misses D2 & D1 '||' D2 ) by A8, A11, A12, A14;
then canonical_embedding (f,d1) = canonical_embedding (f,d2) by A1, A13, A15, Th26;
hence canonical_embedding (f,b1) = canonical_embedding (f,d2) by A10, A11, A14, A15, FINSEQ_3:25; :: thesis:

end;

end;

end;

end;

A16: S₁[ 0 ] by FINSEQ_3:24;
for n being Nat holds S₁[n] from NAT_1:sch 2(A16, A9);
then A17: S₁[ len D] ;
1 in dom D by A5, FUNCT_1:def 2;
then 1 <= len D by FINSEQ_3:25;
hence canonical_embedding (f,b1) = canonical_embedding (f,b2) by A6, A17, FINSEQ_3:25; :: thesis:

end;

suppose B1 meets B2 ; :: thesis:

hence canonical_embedding (f,b1) = canonical_embedding (f,b2) by A4, Th11; :: thesis:

end;

end;