let I be non empty set ; :: thesis: for J being non-Empty TopSpace-yielding ManySortedSet of
for i being Element of I
for xi being Element of (J . i)
for f being Element of (product J) holds f +* i,xi in (proj J,i) " {xi}
let J be non-Empty TopSpace-yielding ManySortedSet of ; :: thesis: for i being Element of I
for xi being Element of (J . i)
for f being Element of (product J) holds f +* i,xi in (proj J,i) " {xi}
let i be Element of I; :: thesis: for xi being Element of (J . i)
for f being Element of (product J) holds f +* i,xi in (proj J,i) " {xi}
let xi be Element of (J . i); :: thesis: for f being Element of (product J) holds f +* i,xi in (proj J,i) " {xi}
let f be Element of (product J); :: thesis: f +* i,xi in (proj J,i) " {xi}
i in I ;
then A1: i in dom (Carrier J) by PARTFUN1:def 4;
xi in the carrier of (J . i) ;
then A2: xi in (Carrier J) . i by YELLOW_6:9;
f in the carrier of (product J) ;
then f in product (Carrier J) by WAYBEL18:def 3;
then f +* i,xi in (proj (Carrier J),i) " {xi} by A1, A2, Th5;
hence f +* i,xi in (proj J,i) " {xi} by WAYBEL18:def 4; :: thesis: verum