let I be non empty set ; :: thesis: for A being ManySortedSet of I
for i, S being set holds {A} +* (i,S) is Segre-like
let A be ManySortedSet of I; :: thesis: for i, S being set holds {A} +* (i,S) is Segre-like
let i, S be set ; :: thesis: {A} +* (i,S) is Segre-like

per cases ( not i in I or i in I ) ;

suppose not i in I ; :: thesis: {A} +* (i,S) is Segre-like

then not i in dom {A} by PARTFUN1:def 2;
hence {A} +* (i,S) is Segre-like by FUNCT_7:def 3; :: thesis: verum

end;

suppose i in I ; :: thesis: {A} +* (i,S) is Segre-like

then reconsider i = i as Element of I ;
take i ; :: according to PENCIL_1:def 20 :: thesis: for j being Element of I st i <> j holds
({A} +* (i,S)) . j is 1 -element
let j be Element of I; :: thesis: ( i <> j implies ({A} +* (i,S)) . j is 1 -element )
assume A1: i <> j ; :: thesis: ({A} +* (i,S)) . j is 1 -element
{A} . j = {(A . j)} by PZFMISC1:def 1;
hence ({A} +* (i,S)) . j is 1 -element by A1, FUNCT_7:32; :: thesis: verum

end;

end;