let I be non empty set ; 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; 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; 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); for f being Element of (product J) holds f +* (i,xi) in (proj (J,i)) " {xi}
let f be Element of (product J); 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; verum