let I be non empty set ; :: thesis: for J being non-Empty TopStruct-yielding ManySortedSet of I

for i1, i2 being Element of I

for xi1 being Element of (J . i1)

for Ai2 being Subset of (J . i2)

for f being Element of (product J) st i1 <> i2 holds

( f in (proj (J,i2)) " Ai2 iff f +* (i1,xi1) in (proj (J,i2)) " Ai2 )

let J be non-Empty TopStruct-yielding ManySortedSet of I; :: thesis: for i1, i2 being Element of I

for xi1 being Element of (J . i1)

for Ai2 being Subset of (J . i2)

for f being Element of (product J) st i1 <> i2 holds

( f in (proj (J,i2)) " Ai2 iff f +* (i1,xi1) in (proj (J,i2)) " Ai2 )

let i1, i2 be Element of I; :: thesis: for xi1 being Element of (J . i1)

for Ai2 being Subset of (J . i2)

for f being Element of (product J) st i1 <> i2 holds

( f in (proj (J,i2)) " Ai2 iff f +* (i1,xi1) in (proj (J,i2)) " Ai2 )

let xi1 be Element of (J . i1); :: thesis: for Ai2 being Subset of (J . i2)

for f being Element of (product J) st i1 <> i2 holds

( f in (proj (J,i2)) " Ai2 iff f +* (i1,xi1) in (proj (J,i2)) " Ai2 )

let Ai2 be Subset of (J . i2); :: thesis: for f being Element of (product J) st i1 <> i2 holds

( f in (proj (J,i2)) " Ai2 iff f +* (i1,xi1) in (proj (J,i2)) " Ai2 )

let f be Element of (product J); :: thesis: ( i1 <> i2 implies ( f in (proj (J,i2)) " Ai2 iff f +* (i1,xi1) in (proj (J,i2)) " Ai2 ) )

reconsider Ai29 = Ai2 as Subset of ((Carrier J) . i2) by YELLOW_6:2;

xi1 in the carrier of (J . i1) ;

then A1: xi1 in (Carrier J) . i1 by YELLOW_6:2;

f in the carrier of (product J) ;

then A2: f in product (Carrier J) by WAYBEL18:def 3;

assume i1 <> i2 ; :: thesis: ( f in (proj (J,i2)) " Ai2 iff f +* (i1,xi1) in (proj (J,i2)) " Ai2 )

then ( f in (proj ((Carrier J),i2)) " Ai29 iff f +* (i1,xi1) in (proj ((Carrier J),i2)) " Ai29 ) by A1, A2, Th6;

hence ( f in (proj (J,i2)) " Ai2 iff f +* (i1,xi1) in (proj (J,i2)) " Ai2 ) by WAYBEL18:def 4; :: thesis: verum

for i1, i2 being Element of I

for xi1 being Element of (J . i1)

for Ai2 being Subset of (J . i2)

for f being Element of (product J) st i1 <> i2 holds

( f in (proj (J,i2)) " Ai2 iff f +* (i1,xi1) in (proj (J,i2)) " Ai2 )

let J be non-Empty TopStruct-yielding ManySortedSet of I; :: thesis: for i1, i2 being Element of I

for xi1 being Element of (J . i1)

for Ai2 being Subset of (J . i2)

for f being Element of (product J) st i1 <> i2 holds

( f in (proj (J,i2)) " Ai2 iff f +* (i1,xi1) in (proj (J,i2)) " Ai2 )

let i1, i2 be Element of I; :: thesis: for xi1 being Element of (J . i1)

for Ai2 being Subset of (J . i2)

for f being Element of (product J) st i1 <> i2 holds

( f in (proj (J,i2)) " Ai2 iff f +* (i1,xi1) in (proj (J,i2)) " Ai2 )

let xi1 be Element of (J . i1); :: thesis: for Ai2 being Subset of (J . i2)

for f being Element of (product J) st i1 <> i2 holds

( f in (proj (J,i2)) " Ai2 iff f +* (i1,xi1) in (proj (J,i2)) " Ai2 )

let Ai2 be Subset of (J . i2); :: thesis: for f being Element of (product J) st i1 <> i2 holds

( f in (proj (J,i2)) " Ai2 iff f +* (i1,xi1) in (proj (J,i2)) " Ai2 )

let f be Element of (product J); :: thesis: ( i1 <> i2 implies ( f in (proj (J,i2)) " Ai2 iff f +* (i1,xi1) in (proj (J,i2)) " Ai2 ) )

reconsider Ai29 = Ai2 as Subset of ((Carrier J) . i2) by YELLOW_6:2;

xi1 in the carrier of (J . i1) ;

then A1: xi1 in (Carrier J) . i1 by YELLOW_6:2;

f in the carrier of (product J) ;

then A2: f in product (Carrier J) by WAYBEL18:def 3;

assume i1 <> i2 ; :: thesis: ( f in (proj (J,i2)) " Ai2 iff f +* (i1,xi1) in (proj (J,i2)) " Ai2 )

then ( f in (proj ((Carrier J),i2)) " Ai29 iff f +* (i1,xi1) in (proj ((Carrier J),i2)) " Ai29 ) by A1, A2, Th6;

hence ( f in (proj (J,i2)) " Ai2 iff f +* (i1,xi1) in (proj (J,i2)) " Ai2 ) by WAYBEL18:def 4; :: thesis: verum