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 (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 I; :: 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)

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;

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 I; :: 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 :: thesis: for o being Element of I holds A . o is connected

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 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;A . o is strongly_connected by A1;

hence A . o is connected by Th4; :: thesis: verum

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 )
;

end;

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

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_{1}[ 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) );

_{1}[ 0 ]
by FINSEQ_3:24;

for n being Nat holds S_{1}[n]
from NAT_1:sch 2(A16, A9);

then A17: S_{1}[ 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: verum

end;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

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 S_{1}[k] holds

S_{1}[k + 1]

A16:
SS

let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A10: S_{1}[k]
; :: thesis: S_{1}[k + 1]

thus S_{1}[k + 1]
:: thesis: verum

end;assume A10: S

thus S

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;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)

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

end;

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

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

end;suppose A14:
1 <= k
; :: thesis: canonical_embedding (f,b1) = canonical_embedding (f,d2)

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: verum

end;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: verum

for n being Nat holds S

then A17: S

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: verum