let I be non empty set ; :: thesis: for A being PLS-yielding ManySortedSet of
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 ; :: 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 A2: ( C1 = f .: B1 & 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 set such that
A3: ( a in dom f & a in B1 & x = f . a ) by A2, FUNCT_1:def 12;
reconsider a = a as Point of (Segre_Product A) by A3;
consider b being Point of (Segre_Product A) such that
A4: ( b in B2 & a,b are_collinear ) by A1, A3, Def2;
A5: dom f = the carrier of (Segre_Product A) by FUNCT_2:def 1;
take y = f . b; :: thesis: ( y in C2 & x,y are_collinear )
thus y in C2 by A2, A4, A5, FUNCT_1:def 12; :: 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 A3, 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
A6: {a,b} c= l by A4, PENCIL_1:def 1;
reconsider k = f .: l as Block of (Segre_Product A) ;
( a in l & b in l ) by A6, ZFMISC_1:38;
then ( x in k & y in k ) by A3, A5, FUNCT_1:def 12;
then {x,y} c= k by ZFMISC_1:38;
hence x,y are_collinear by PENCIL_1:def 1; :: thesis: verum

end;

end;