let I be non empty set ; :: thesis: for J being non-Empty TopSpace-yielding ManySortedSet of
for i1, i2 being Element of I
for xi1 being Element of (J . i1)
for Ai2 being Subset of (J . i2) st Ai2 <> [#] (J . i2) holds
( (proj J,i1) " {xi1} c= (proj J,i2) " Ai2 iff ( i1 = i2 & xi1 in Ai2 ) )
let J be non-Empty TopSpace-yielding ManySortedSet of ; :: thesis: for i1, i2 being Element of I
for xi1 being Element of (J . i1)
for Ai2 being Subset of (J . i2) st Ai2 <> [#] (J . i2) holds
( (proj J,i1) " {xi1} c= (proj J,i2) " Ai2 iff ( i1 = i2 & xi1 in Ai2 ) )
let i1, i2 be Element of I; :: thesis: for xi1 being Element of (J . i1)
for Ai2 being Subset of (J . i2) st Ai2 <> [#] (J . i2) holds
( (proj J,i1) " {xi1} c= (proj J,i2) " Ai2 iff ( i1 = i2 & xi1 in Ai2 ) )
let xi1 be Element of (J . i1); :: thesis: for Ai2 being Subset of (J . i2) st Ai2 <> [#] (J . i2) holds
( (proj J,i1) " {xi1} c= (proj J,i2) " Ai2 iff ( i1 = i2 & xi1 in Ai2 ) )
let Ai2 be Subset of (J . i2); :: thesis: ( Ai2 <> [#] (J . i2) implies ( (proj J,i1) " {xi1} c= (proj J,i2) " Ai2 iff ( i1 = i2 & xi1 in Ai2 ) ) )
A1: product (Carrier J) <> {} ;
i1 in I ;
then A2: i1 in dom (Carrier J) by PARTFUN1:def 4;
i2 in I ;
then A3: i2 in dom (Carrier J) by PARTFUN1:def 4;
assume A4: Ai2 <> [#] (J . i2) ; :: thesis: ( (proj J,i1) " {xi1} c= (proj J,i2) " Ai2 iff ( i1 = i2 & xi1 in Ai2 ) )
xi1 in the carrier of (J . i1) ;
then A5: xi1 in (Carrier J) . i1 by YELLOW_6:9;
reconsider Ai2' = Ai2 as Subset of ((Carrier J) . i2) by YELLOW_6:9;
Ai2 <> the carrier of (J . i2) by A4;
then Ai2' <> (Carrier J) . i2 by YELLOW_6:9;
then ( (proj (Carrier J),i1) " {xi1} c= (proj (Carrier J),i2) " Ai2' iff ( i1 = i2 & xi1 in Ai2' ) ) by A1, A2, A3, A5, Th7;
then ( (proj J,i1) " {xi1} c= (proj (Carrier J),i2) " Ai2 iff ( i1 = i2 & xi1 in Ai2' ) ) by WAYBEL18:def 4;
hence ( (proj J,i1) " {xi1} c= (proj J,i2) " Ai2 iff ( i1 = i2 & xi1 in Ai2 ) ) by WAYBEL18:def 4; :: thesis: verum