let I be non empty set ; :: thesis: for A being PLS-yielding ManySortedSet of I

for B1, B2 being Segre-Coset of A st B1 '||' B2 holds

for f being Collineation of (Segre_Product A)

for C1, C2 being Segre-Coset of A st C1 = f .: B1 & C2 = f .: B2 holds

C1 '||' C2

let A be PLS-yielding ManySortedSet of I; :: thesis: for B1, B2 being Segre-Coset of A st B1 '||' B2 holds

for f being Collineation of (Segre_Product A)

for C1, C2 being Segre-Coset of A st C1 = f .: B1 & C2 = f .: B2 holds

C1 '||' C2

let B1, B2 be Segre-Coset of A; :: thesis: ( B1 '||' B2 implies for f being Collineation of (Segre_Product A)

for C1, C2 being Segre-Coset of A st C1 = f .: B1 & C2 = f .: B2 holds

C1 '||' C2 )

assume A1: B1 '||' B2 ; :: thesis: for f being Collineation of (Segre_Product A)

for C1, C2 being Segre-Coset of A st C1 = f .: B1 & C2 = f .: B2 holds

C1 '||' C2

let f be Collineation of (Segre_Product A); :: thesis: for C1, C2 being Segre-Coset of A st C1 = f .: B1 & C2 = f .: B2 holds

C1 '||' C2

let C1, C2 be Segre-Coset of A; :: thesis: ( C1 = f .: B1 & C2 = f .: B2 implies C1 '||' C2 )

assume that

A2: C1 = f .: B1 and

A3: C2 = f .: B2 ; :: thesis: C1 '||' C2

let x be Point of (Segre_Product A); :: according to PENCIL_3:def 2 :: thesis: ( x in C1 implies ex y being Point of (Segre_Product A) st

( y in C2 & x,y are_collinear ) )

assume x in C1 ; :: thesis: ex y being Point of (Segre_Product A) st

( y in C2 & x,y are_collinear )

then consider a being object such that

A4: a in dom f and

A5: a in B1 and

A6: x = f . a by A2, FUNCT_1:def 6;

reconsider a = a as Point of (Segre_Product A) by A4;

consider b being Point of (Segre_Product A) such that

A7: b in B2 and

A8: a,b are_collinear by A1, A5;

take y = f . b; :: thesis: ( y in C2 & x,y are_collinear )

A9: dom f = the carrier of (Segre_Product A) by FUNCT_2:def 1;

hence y in C2 by A3, A7, FUNCT_1:def 6; :: thesis: x,y are_collinear

for B1, B2 being Segre-Coset of A st B1 '||' B2 holds

for f being Collineation of (Segre_Product A)

for C1, C2 being Segre-Coset of A st C1 = f .: B1 & C2 = f .: B2 holds

C1 '||' C2

let A be PLS-yielding ManySortedSet of I; :: thesis: for B1, B2 being Segre-Coset of A st B1 '||' B2 holds

for f being Collineation of (Segre_Product A)

for C1, C2 being Segre-Coset of A st C1 = f .: B1 & C2 = f .: B2 holds

C1 '||' C2

let B1, B2 be Segre-Coset of A; :: thesis: ( B1 '||' B2 implies for f being Collineation of (Segre_Product A)

for C1, C2 being Segre-Coset of A st C1 = f .: B1 & C2 = f .: B2 holds

C1 '||' C2 )

assume A1: B1 '||' B2 ; :: thesis: for f being Collineation of (Segre_Product A)

for C1, C2 being Segre-Coset of A st C1 = f .: B1 & C2 = f .: B2 holds

C1 '||' C2

let f be Collineation of (Segre_Product A); :: thesis: for C1, C2 being Segre-Coset of A st C1 = f .: B1 & C2 = f .: B2 holds

C1 '||' C2

let C1, C2 be Segre-Coset of A; :: thesis: ( C1 = f .: B1 & C2 = f .: B2 implies C1 '||' C2 )

assume that

A2: C1 = f .: B1 and

A3: C2 = f .: B2 ; :: thesis: C1 '||' C2

let x be Point of (Segre_Product A); :: according to PENCIL_3:def 2 :: thesis: ( x in C1 implies ex y being Point of (Segre_Product A) st

( y in C2 & x,y are_collinear ) )

assume x in C1 ; :: thesis: ex y being Point of (Segre_Product A) st

( y in C2 & x,y are_collinear )

then consider a being object such that

A4: a in dom f and

A5: a in B1 and

A6: x = f . a by A2, FUNCT_1:def 6;

reconsider a = a as Point of (Segre_Product A) by A4;

consider b being Point of (Segre_Product A) such that

A7: b in B2 and

A8: a,b are_collinear by A1, A5;

take y = f . b; :: thesis: ( y in C2 & x,y are_collinear )

A9: dom f = the carrier of (Segre_Product A) by FUNCT_2:def 1;

hence y in C2 by A3, A7, FUNCT_1:def 6; :: thesis: x,y are_collinear

per cases
( a = b or a <> b )
;

end;

suppose
a <> b
; :: thesis: x,y are_collinear

then consider l being Block of (Segre_Product A) such that

A10: {a,b} c= l by A8, PENCIL_1:def 1;

reconsider k = f .: l as Block of (Segre_Product A) ;

b in l by A10, ZFMISC_1:32;

then A11: y in k by A9, FUNCT_1:def 6;

a in l by A10, ZFMISC_1:32;

then x in k by A4, A6, FUNCT_1:def 6;

then {x,y} c= k by A11, ZFMISC_1:32;

hence x,y are_collinear by PENCIL_1:def 1; :: thesis: verum

end;A10: {a,b} c= l by A8, PENCIL_1:def 1;

reconsider k = f .: l as Block of (Segre_Product A) ;

b in l by A10, ZFMISC_1:32;

then A11: y in k by A9, FUNCT_1:def 6;

a in l by A10, ZFMISC_1:32;

then x in k by A4, A6, FUNCT_1:def 6;

then {x,y} c= k by A11, ZFMISC_1:32;

hence x,y are_collinear by PENCIL_1:def 1; :: thesis: verum