let I be non empty set ; :: thesis: for A being PLS-yielding ManySortedSet of
for P being ManySortedSet of st P is Point of (Segre_Product A) holds
for i being Element of I
for p being Point of (A . i) holds P +* i,p is Point of (Segre_Product A)
let A be PLS-yielding ManySortedSet of ; :: thesis: for P being ManySortedSet of st P is Point of (Segre_Product A) holds
for i being Element of I
for p being Point of (A . i) holds P +* i,p is Point of (Segre_Product A)
let P be ManySortedSet of ; :: thesis: ( P is Point of (Segre_Product A) implies for i being Element of I
for p being Point of (A . i) holds P +* i,p is Point of (Segre_Product A) )
assume A1: P is Point of (Segre_Product A) ; :: thesis: for i being Element of I
for p being Point of (A . i) holds P +* i,p is Point of (Segre_Product A)
let j be Element of I; :: thesis: for p being Point of (A . j) holds P +* j,p is Point of (Segre_Product A)
let p be Point of (A . j); :: thesis: P +* j,p is Point of (Segre_Product A)
A2: dom (P +* j,p) = I by PARTFUN1:def 4
.= dom (Carrier A) by PARTFUN1:def 4 ;
for i being set st i in dom (Carrier A) holds
(P +* j,p) . i in (Carrier A) . i

proof

let i be set ; :: thesis: ( i in dom (Carrier A) implies (P +* j,p) . i in (Carrier A) . i )
assume A3: i in dom (Carrier A) ; :: thesis: (P +* j,p) . i in (Carrier A) . i
then i in I by PARTFUN1:def 4;
then A4: i in dom P by PARTFUN1:def 4;

per cases ( i <> j or i = j ) ;

suppose i <> j ; :: thesis: (P +* j,p) . i in (Carrier A) . i

then (P +* j,p) . i = P . i by FUNCT_7:34;
hence (P +* j,p) . i in (Carrier A) . i by A1, A3, CARD_3:18; :: thesis: verum

end;

suppose A5: i = j ; :: thesis: (P +* j,p) . i in (Carrier A) . i

then A6: (P +* j,p) . i = p by A4, FUNCT_7:33;
p in the carrier of (A . j) ;
hence (P +* j,p) . i in (Carrier A) . i by A5, A6, YELLOW_6:9; :: thesis: verum

end;

end;

end;

hence P +* j,p is Point of (Segre_Product A) by A2, CARD_3:18; :: thesis: verum