let I be non empty set ; :: thesis: for J being non-Empty TopStruct-yielding ManySortedSet of I
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 TopStruct-yielding ManySortedSet of I; :: 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}
xi in the carrier of (J . i) ;
then A1: xi in (Carrier J) . i by YELLOW_6:2;
f in the carrier of (product J) ;
then A2: f in product (Carrier J) by WAYBEL18:def 3;
i in I ;
then i in dom (Carrier J) by PARTFUN1:def 2;
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