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

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

suppose a = b ; :: thesis: x,y are_collinear

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

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;

end;