let I be non empty set ; :: thesis: for A being PLS-yielding ManySortedSet of I
for P being ManySortedSet of I 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 I; :: thesis: for P being ManySortedSet of I 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 I; :: 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: for i being object st i in dom (Carrier A) holds
(P +* (j,p)) . i in (Carrier A) . i

proof

let i be object ; :: 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 2;
then A4: i in dom P by PARTFUN1:def 2;

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:32;
hence (P +* (j,p)) . i in (Carrier A) . i by A1, A3, CARD_3:9; :: thesis: verum

end;

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

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

end;

end;

end;

dom (P +* (j,p)) = I by PARTFUN1:def 2
.= dom (Carrier A) by PARTFUN1:def 2 ;
hence P +* (j,p) is Point of (Segre_Product A) by A2, CARD_3:9; :: thesis: verum