let I be non empty set ; :: thesis: for J being non-Empty TopSpace-yielding ManySortedSet of I
for i1, i2 being Element of I
for xi1 being Element of
for Ai2 being Subset of
for f being Element of st i1 <> i2 holds
( f in (proj J,i2) " Ai2 iff f +* i1,xi1 in (proj J,i2) " Ai2 )
let J be non-Empty TopSpace-yielding ManySortedSet of I; :: thesis: for i1, i2 being Element of I
for xi1 being Element of
for Ai2 being Subset of
for f being Element of 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
for Ai2 being Subset of
for f being Element of st i1 <> i2 holds
( f in (proj J,i2) " Ai2 iff f +* i1,xi1 in (proj J,i2) " Ai2 )
let xi1 be Element of ; :: thesis: for Ai2 being Subset of
for f being Element of st i1 <> i2 holds
( f in (proj J,i2) " Ai2 iff f +* i1,xi1 in (proj J,i2) " Ai2 )
let Ai2 be Subset of ; :: thesis: for f being Element of st i1 <> i2 holds
( f in (proj J,i2) " Ai2 iff f +* i1,xi1 in (proj J,i2) " Ai2 )
let f be Element of ; :: thesis: ( i1 <> i2 implies ( f in (proj J,i2) " Ai2 iff f +* i1,xi1 in (proj J,i2) " Ai2 ) )
reconsider Ai2' = Ai2 as Subset of by YELLOW_6:9;
xi1 in the carrier of (J . i1) ;
then A1: xi1 in (Carrier J) . i1 by YELLOW_6:9;
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) " Ai2' iff f +* i1,xi1 in (proj (Carrier J),i2) " Ai2' ) 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