let I be non empty finite set ; :: thesis: for A being PLS-yielding ManySortedSet of 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 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 ; :: thesis: ( ( 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 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 (Segre_Product A)
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

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 (Segre_Product A); :: 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 A3: ( product b1 is Segre-Coset of A & product b2 is Segre-Coset of A & 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 (Segre_Product A) such that
A4: ( D . 1 = B1 & D . (len D) = B2 & ( for i being Nat st i in dom D holds
D . i is Segre-Coset of A ) & ( 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, 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 );
A5: S₁[ 0 ] by FINSEQ_3:26;

A6: now

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A7: S₁[k] ; :: thesis: S₁[k + 1]
thus S₁[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:27;
then A8: 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 A9: 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 A10: D2 = product d2 ; :: thesis: canonical_embedding f,b1 = canonical_embedding f,d2

per cases ( k = 0 or 1 <= k ) by NAT_1:14;

suppose k = 0 ; :: thesis: canonical_embedding f,b1 = canonical_embedding f,d2

hence canonical_embedding f,b1 = canonical_embedding f,d2 by A4, A9, A10, PUA2MSS1:2; :: thesis: verum

end;

suppose A11: 1 <= k ; :: thesis: canonical_embedding f,b1 = canonical_embedding f,d2

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

end;

end;

end;

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A5, A6);
then A13: S₁[ len D] ;
1 in dom D by A4, FUNCT_1:def 4;
then 1 <= len D by FINSEQ_3:27;
hence canonical_embedding f,b1 = canonical_embedding f,b2 by A4, A13, FINSEQ_3:27; :: thesis: verum

end;

suppose B1 meets B2 ; :: thesis: canonical_embedding f,b1 = canonical_embedding f,b2

hence canonical_embedding f,b1 = canonical_embedding f,b2 by A3, Th11; :: thesis: verum

end;

end;