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 holds
for i being Element of I
for p being Point of holds P +* i,p is Point of
let A be PLS-yielding ManySortedSet of I; :: thesis: for P being ManySortedSet of I st P is Point of holds
for i being Element of I
for p being Point of holds P +* i,p is Point of
let P be ManySortedSet of I; :: thesis: ( P is Point of implies for i being Element of I
for p being Point of holds P +* i,p is Point of )
assume A1: P is Point of ; :: thesis: for i being Element of I
for p being Point of holds P +* i,p is Point of
let j be Element of I; :: thesis: for p being Point of holds P +* j,p is Point of
let p be Point of ; :: thesis: P +* j,p is Point of
A2: 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

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

end;

end;

end;

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