let I be non empty set ; :: thesis: for A being PLS-yielding ManySortedSet of 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 ; :: 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
f is bijective by Def4;
then A2: ( f is one-to-one & f is onto ) ;
then A3: rng f = [#] (Segre_Product A) by FUNCT_2:def 3;
reconsider g = f " as Collineation of (Segre_Product A) by Th13;
f " B = g .: B by A2, A3, TOPS_2:68;
hence f " B is Segre-Coset of A by A1, Th24; :: thesis: verum