let I be non empty 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 B being Segre-Coset of A

for f being Collineation of (Segre_Product A) holds f " B is Segre-Coset of A

let A be PLS-yielding ManySortedSet of I; :: thesis: ( ( for i being Element of I holds A . i is strongly_connected ) implies for B being Segre-Coset of A

for f being Collineation of (Segre_Product A) holds f " B is Segre-Coset of A )

assume A1: for i being Element of I holds A . i is strongly_connected ; :: thesis: for B being Segre-Coset of A

for f being Collineation of (Segre_Product A) holds f " B is Segre-Coset of A

let B be Segre-Coset of A; :: thesis: for f being Collineation of (Segre_Product A) holds f " B is Segre-Coset of A

let f be Collineation of (Segre_Product A); :: thesis: f " B is Segre-Coset of A

reconsider g = f " as Collineation of (Segre_Product A) by Th13;

A2: f is bijective by Def4;

then rng f = [#] (Segre_Product A) by FUNCT_2:def 3;

then f " B = g .: B by A2, TOPS_2:55;

hence f " B is Segre-Coset of A by A1, Th24; :: thesis: verum

for B being Segre-Coset of A

for f being Collineation of (Segre_Product A) holds f " B is Segre-Coset of A

let A be PLS-yielding ManySortedSet of I; :: thesis: ( ( for i being Element of I holds A . i is strongly_connected ) implies for B being Segre-Coset of A

for f being Collineation of (Segre_Product A) holds f " B is Segre-Coset of A )

assume A1: for i being Element of I holds A . i is strongly_connected ; :: thesis: for B being Segre-Coset of A

for f being Collineation of (Segre_Product A) holds f " B is Segre-Coset of A

let B be Segre-Coset of A; :: thesis: for f being Collineation of (Segre_Product A) holds f " B is Segre-Coset of A

let f be Collineation of (Segre_Product A); :: thesis: f " B is Segre-Coset of A

reconsider g = f " as Collineation of (Segre_Product A) by Th13;

A2: f is bijective by Def4;

then rng f = [#] (Segre_Product A) by FUNCT_2:def 3;

then f " B = g .: B by A2, TOPS_2:55;

hence f " B is Segre-Coset of A by A1, Th24; :: thesis: verum