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 Segre-Coset of A st B1 misses B2 & B1 '||' B2 holds
for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b1 = B1 & product b2 = 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 Segre-Coset of A st B1 misses B2 & B1 '||' B2 holds
for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b1 = B1 & product b2 = 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 Segre-Coset of A st B1 misses B2 & B1 '||' B2 holds
for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b1 = B1 & product b2 = B2 holds
canonical_embedding (f,b1) = canonical_embedding (f,b2)

let f be Collineation of (); :: thesis: for B1, B2 being Segre-Coset of A st B1 misses B2 & B1 '||' B2 holds
for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b1 = B1 & product b2 = B2 holds
canonical_embedding (f,b1) = canonical_embedding (f,b2)

let B1, B2 be Segre-Coset of A; :: thesis: ( B1 misses B2 & B1 '||' B2 implies for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b1 = B1 & product b2 = B2 holds
canonical_embedding (f,b1) = canonical_embedding (f,b2) )

assume that
A2: B1 misses B2 and
A3: B1 '||' B2 ; :: thesis: for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b1 = B1 & product b2 = 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 = B1 & product b2 = B2 implies canonical_embedding (f,b1) = canonical_embedding (f,b2) )
assume that
A4: product b1 = B1 and
A5: product b2 = B2 ; :: thesis: canonical_embedding (f,b1) = canonical_embedding (f,b2)
A6: indx b1 = indx b2 by A2, A3, A4, A5, Th21;
reconsider B3 = f .: B1, B4 = f .: B2 as Segre-Coset of A by ;
A7: f is bijective by PENCIL_2:def 4;
then A8: B3 misses B4 by ;
set i = indx b1;
consider r being Element of I such that
A9: r <> indx b1 and
A10: for i being Element of I st i <> r holds
b1 . i = b2 . i and
A11: for c1, c2 being Point of (A . r) st b1 . r = {c1} & b2 . r = {c2} holds
c1,c2 are_collinear by A2, A3, A4, A5, Th21;
consider b4 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that
A12: product b4 = B4 and
A13: b4 . (indx b4) = [#] (A . (indx b4)) by PENCIL_2:def 2;
consider b3 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that
A14: product b3 = B3 and
A15: b3 . (indx b3) = [#] (A . (indx b3)) by PENCIL_2:def 2;
B3 '||' B4 by ;
then A16: indx b3 = indx b4 by A8, A14, A12, Th21;
set j = indx b3;
A17: dom f = the carrier of () by FUNCT_2:def 1;
A18: dom b1 = I by PARTFUN1:def 2;
A19: now :: thesis: for o being object st o in the carrier of (A . (indx b1)) holds
(canonical_embedding (f,b1)) . o = (canonical_embedding (f,b2)) . o
b2 . r is trivial by ;
then consider c2 being object such that
A20: b2 . r = {c2} by ZFMISC_1:131;
b2 c= Carrier A by PBOOLE:def 18;
then b2 . r c= () . r ;
then A21: {c2} c= [#] (A . r) by ;
let o be object ; :: thesis: ( o in the carrier of (A . (indx b1)) implies (canonical_embedding (f,b1)) . b1 = (canonical_embedding (f,b2)) . b1 )
consider p0 being object such that
A22: p0 in product b1 by XBOOLE_0:def 1;
assume o in the carrier of (A . (indx b1)) ; :: thesis: (canonical_embedding (f,b1)) . b1 = (canonical_embedding (f,b2)) . b1
then reconsider u = o as Point of (A . (indx b1)) ;
reconsider p1 = p0 as Point of () by ;
reconsider p = p1 as ManySortedSet of I by PENCIL_1:14;
set q = p +* ((indx b1),u);
reconsider q1 = p +* ((indx b1),u) as Point of () by PENCIL_1:25;
b1 . r is trivial by ;
then consider c1 being object such that
A23: b1 . r = {c1} by ZFMISC_1:131;
b1 c= Carrier A by PBOOLE:def 18;
then b1 . r c= () . r ;
then {c1} c= [#] (A . r) by ;
then reconsider c1 = c1 as Point of (A . r) by ZFMISC_1:31;
reconsider c2 = c2 as Point of (A . r) by ;
set t = (p +* ((indx b1),u)) +* (r,c2);
p +* ((indx b1),u) is Point of () by PENCIL_1:25;
then reconsider t1 = (p +* ((indx b1),u)) +* (r,c2) as Point of () by PENCIL_1:25;
per cases ( c1 <> c2 or c1 = c2 ) ;
suppose A24: c1 <> c2 ; :: thesis: (canonical_embedding (f,b1)) . b1 = (canonical_embedding (f,b2)) . b1
(p +* ((indx b1),u)) . r = p . r by ;
then (p +* ((indx b1),u)) . r in b1 . r by ;
then A25: (p +* ((indx b1),u)) . r = c1 by ;
dom (p +* ((indx b1),u)) = I by PARTFUN1:def 2;
then A26: ((p +* ((indx b1),u)) +* (r,c2)) . r = c2 by FUNCT_7:31;
now :: thesis: for q3, t3 being ManySortedSet of I st q3 = q1 & t3 = t1 holds
ex r being Element of I st
( ( for a, b being Point of (A . r) st a = q3 . r & b = t3 . r holds
( a <> b & a,b are_collinear ) ) & ( for j being Element of I st j <> r holds
q3 . j = t3 . j ) )
let q3, t3 be ManySortedSet of I; :: thesis: ( q3 = q1 & t3 = t1 implies ex r being Element of I st
( ( for a, b being Point of (A . r) st a = q3 . r & b = t3 . r holds
( a <> b & a,b are_collinear ) ) & ( for j being Element of I st j <> r holds
q3 . j = t3 . j ) ) )

assume A27: ( q3 = q1 & t3 = t1 ) ; :: thesis: ex r being Element of I st
( ( for a, b being Point of (A . r) st a = q3 . r & b = t3 . r holds
( a <> b & a,b are_collinear ) ) & ( for j being Element of I st j <> r holds
q3 . j = t3 . j ) )

take r = r; :: thesis: ( ( for a, b being Point of (A . r) st a = q3 . r & b = t3 . r holds
( a <> b & a,b are_collinear ) ) & ( for j being Element of I st j <> r holds
q3 . j = t3 . j ) )

thus for a, b being Point of (A . r) st a = q3 . r & b = t3 . r holds
( a <> b & a,b are_collinear ) by A11, A23, A20, A24, A25, A26, A27; :: thesis: for j being Element of I st j <> r holds
q3 . j = t3 . j

let j be Element of I; :: thesis: ( j <> r implies q3 . j = t3 . j )
assume j <> r ; :: thesis: q3 . j = t3 . j
hence q3 . j = t3 . j by ; :: thesis: verum
end;
then q1,t1 are_collinear by ;
then A28: f . q1,f . t1 are_collinear by Th1;
reconsider fq = f . q1, ft = f . t1 as ManySortedSet of I by PENCIL_1:14;
A29: dom b1 = I by PARTFUN1:def 2;
A30: dom p = I by PARTFUN1:def 2;
A31: now :: thesis: for a being object st a in I holds
(p +* ((indx b1),u)) . a in b1 . a
let a be object ; :: thesis: ( a in I implies (p +* ((indx b1),u)) . b1 in b1 . b1 )
assume A32: a in I ; :: thesis: (p +* ((indx b1),u)) . b1 in b1 . b1
per cases ( a = indx b1 or a <> indx b1 ) ;
suppose a = indx b1 ; :: thesis: (p +* ((indx b1),u)) . b1 in b1 . b1
then ( (p +* ((indx b1),u)) . a = u & b1 . a = [#] (A . (indx b1)) ) by ;
hence (p +* ((indx b1),u)) . a in b1 . a ; :: thesis: verum
end;
suppose a <> indx b1 ; :: thesis: (p +* ((indx b1),u)) . b1 in b1 . b1
then (p +* ((indx b1),u)) . a = p . a by FUNCT_7:32;
hence (p +* ((indx b1),u)) . a in b1 . a by ; :: thesis: verum
end;
end;
end;
A33: dom (p +* ((indx b1),u)) = I by PARTFUN1:def 2;
then A34: p +* ((indx b1),u) in product b1 by ;
A35: now :: thesis: for a being object st a in I holds
((p +* ((indx b1),u)) +* (r,c2)) . a in b2 . a
let a be object ; :: thesis: ( a in I implies ((p +* ((indx b1),u)) +* (r,c2)) . b1 in b2 . b1 )
assume A36: a in I ; :: thesis: ((p +* ((indx b1),u)) +* (r,c2)) . b1 in b2 . b1
per cases ( a = r or a <> r ) ;
suppose A37: a = r ; :: thesis: ((p +* ((indx b1),u)) +* (r,c2)) . b1 in b2 . b1
then ((p +* ((indx b1),u)) +* (r,c2)) . a = c2 by ;
hence ((p +* ((indx b1),u)) +* (r,c2)) . a in b2 . a by ; :: thesis: verum
end;
suppose A38: a <> r ; :: thesis: ((p +* ((indx b1),u)) +* (r,c2)) . b1 in b2 . b1
then ((p +* ((indx b1),u)) +* (r,c2)) . a = (p +* ((indx b1),u)) . a by FUNCT_7:32;
then ((p +* ((indx b1),u)) +* (r,c2)) . a in b1 . a by ;
hence ((p +* ((indx b1),u)) +* (r,c2)) . a in b2 . a by ; :: thesis: verum
end;
end;
end;
( dom ((p +* ((indx b1),u)) +* (r,c2)) = I & dom b2 = I ) by PARTFUN1:def 2;
then A39: (p +* ((indx b1),u)) +* (r,c2) in product b2 by ;
then A40: (canonical_embedding (f,b2)) . (((p +* ((indx b1),u)) +* (r,c2)) . (indx b1)) = ft . ( . (indx b1)) by A1, A5, A6, Def4;
A41: f . q1 <> f . t1 by ;
A42: now :: thesis: not fq . (indx b3) <> ft . (indx b3)
consider l being Element of I such that
for a, b being Point of (A . l) st a = fq . l & b = ft . l holds
( a <> b & a,b are_collinear ) and
A43: for j being Element of I st j <> l holds
fq . j = ft . j by ;
assume fq . (indx b3) <> ft . (indx b3) ; :: thesis: contradiction
then A44: indx b3 = l by A43;
A45: dom b4 = I by PARTFUN1:def 2;
A46: fq in B3 by ;
A47: dom b3 = I by PARTFUN1:def 2;
A48: now :: thesis: for o being object st o in I holds
fq . o in b4 . o
let o be object ; :: thesis: ( o in I implies fq . b1 in b4 . b1 )
assume o in I ; :: thesis: fq . b1 in b4 . b1
then reconsider o1 = o as Element of I ;
per cases ( o1 = indx b3 or o1 <> indx b3 ) ;
suppose o1 = indx b3 ; :: thesis: fq . b1 in b4 . b1
hence fq . o in b4 . o by ; :: thesis: verum
end;
suppose o1 <> indx b3 ; :: thesis: fq . b1 in b4 . b1
then A49: fq . o1 = ft . o1 by ;
ft in product b4 by ;
hence fq . o in b4 . o by ; :: thesis: verum
end;
end;
end;
dom fq = I by PARTFUN1:def 2;
then fq in product b4 by ;
then fq in (product b3) /\ (product b4) by ;
hence contradiction by A8, A14, A12; :: thesis: verum
end;
A50: indx b3 = . (indx b1) by A1, A4, A14, Def3;
dom p = I by PARTFUN1:def 2;
then A51: (p +* ((indx b1),u)) . (indx b1) = o by FUNCT_7:31;
then ((p +* ((indx b1),u)) +* (r,c2)) . (indx b1) = o by ;
hence (canonical_embedding (f,b1)) . o = (canonical_embedding (f,b2)) . o by A1, A4, A50, A34, A40, A42, A51, Def4; :: thesis: verum
end;
suppose A52: c1 = c2 ; :: thesis: (canonical_embedding (f,b1)) . b1 = (canonical_embedding (f,b2)) . b1
A53: now :: thesis: for o being object st o in I holds
b1 . o = b2 . o
let o be object ; :: thesis: ( o in I implies b1 . b1 = b2 . b1 )
assume o in I ; :: thesis: b1 . b1 = b2 . b1
then reconsider o1 = o as Element of I ;
per cases ( r = o1 or r <> o1 ) ;
suppose r = o1 ; :: thesis: b1 . b1 = b2 . b1
hence b1 . o = b2 . o by ; :: thesis: verum
end;
suppose r <> o1 ; :: thesis: b1 . b1 = b2 . b1
hence b1 . o = b2 . o by A10; :: thesis: verum
end;
end;
end;
( dom b1 = I & dom b2 = I ) by PARTFUN1:def 2;
hence (canonical_embedding (f,b1)) . o = (canonical_embedding (f,b2)) . o by ; :: thesis: verum
end;
end;
end;
( dom (canonical_embedding (f,b1)) = the carrier of (A . (indx b1)) & dom (canonical_embedding (f,b2)) = the carrier of (A . (indx b1)) ) by ;
hence canonical_embedding (f,b1) = canonical_embedding (f,b2) by A19; :: thesis: verum