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

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