let I be non empty set ; :: thesis: for J being non-Empty TopSpace-yielding ManySortedSet of I
for i being Element of I
for P being Subset of (J . i) holds (proj J,i) " P = product ((Carrier J) +* i,P)
let J be non-Empty TopSpace-yielding ManySortedSet of I; :: thesis: for i being Element of I
for P being Subset of (J . i) holds (proj J,i) " P = product ((Carrier J) +* i,P)
let i be Element of I; :: thesis: for P being Subset of (J . i) holds (proj J,i) " P = product ((Carrier J) +* i,P)
let P be Subset of (J . i); :: thesis: (proj J,i) " P = product ((Carrier J) +* i,P)
set f = (Carrier J) +* i,P;
A1: dom (Carrier J) = I by PARTFUN1:def 4;
A2: dom ((Carrier J) +* i,P) = dom (Carrier J) by FUNCT_7:32
.= I by PARTFUN1:def 4 ;
A3: product ((Carrier J) +* i,P) c= (proj J,i) " P

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in product ((Carrier J) +* i,P) or x in (proj J,i) " P )
assume x in product ((Carrier J) +* i,P) ; :: thesis: x in (proj J,i) " P
then consider g being Function such that
A4: x = g and
A5: dom g = dom ((Carrier J) +* i,P) and
A6: for y being set st y in dom ((Carrier J) +* i,P) holds
g . y in ((Carrier J) +* i,P) . y by CARD_3:def 5;
A7: for j being set st j in dom (Carrier J) holds
g . j in (Carrier J) . j

proof

let j be set ; :: thesis: ( j in dom (Carrier J) implies g . j in (Carrier J) . j )
assume j in dom (Carrier J) ; :: thesis: g . j in (Carrier J) . j
then A8: j in I by PARTFUN1:def 4;
then A9: ex R being 1-sorted st
( R = J . j & (Carrier J) . j = the carrier of R ) by PRALG_1:def 13;

per cases ( j = i or j <> i ) ;

suppose A10: j = i ; :: thesis: g . j in (Carrier J) . j

((Carrier J) +* i,P) . i = P by A1, FUNCT_7:33;
then g . j in P by A2, A6, A10;
hence g . j in (Carrier J) . j by A9, A10; :: thesis: verum

end;

suppose j <> i ; :: thesis: g . j in (Carrier J) . j

then ((Carrier J) +* i,P) . j = (Carrier J) . j by FUNCT_7:34;
hence g . j in (Carrier J) . j by A2, A6, A8; :: thesis: verum

end;

end;

end;

dom g = dom (Carrier J) by A5, FUNCT_7:32;
then A11: g in product (Carrier J) by A7, CARD_3:18;
then A12: g in dom (proj (Carrier J),i) by CARD_3:def 17;
((Carrier J) +* i,P) . i = P by A1, FUNCT_7:33;
then g . i in P by A2, A6;
then A13: (proj (Carrier J),i) . g in P by A12, CARD_3:def 17;
g in dom (proj J,i) by A11, CARD_3:def 17;
hence x in (proj J,i) " P by A4, A13, FUNCT_1:def 13; :: thesis: verum

end;

(proj J,i) " P c= product ((Carrier J) +* i,P)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (proj J,i) " P or x in product ((Carrier J) +* i,P) )
assume A14: x in (proj J,i) " P ; :: thesis: x in product ((Carrier J) +* i,P)
then A15: x in dom (proj (Carrier J),i) by FUNCT_1:def 13;
then x in product (Carrier J) by CARD_3:def 17;
then consider g being Function such that
A16: x = g and
A17: dom g = dom (Carrier J) and
A18: for y being set st y in dom (Carrier J) holds
g . y in (Carrier J) . y by CARD_3:def 5;
A19: dom g = dom ((Carrier J) +* i,P) by A17, FUNCT_7:32;
for j being set st j in dom ((Carrier J) +* i,P) holds
g . j in ((Carrier J) +* i,P) . j

proof

let j be set ; :: thesis: ( j in dom ((Carrier J) +* i,P) implies g . j in ((Carrier J) +* i,P) . j )
assume j in dom ((Carrier J) +* i,P) ; :: thesis: g . j in ((Carrier J) +* i,P) . j
then A20: g . j in (Carrier J) . j by A17, A18, A19;

per cases ( i = j or i <> j ) ;

suppose A21: i = j ; :: thesis: g . j in ((Carrier J) +* i,P) . j

(proj (Carrier J),i) . x = g . i by A15, A16, CARD_3:def 17;
then g . i in P by A14, FUNCT_1:def 13;
hence g . j in ((Carrier J) +* i,P) . j by A1, A21, FUNCT_7:33; :: thesis: verum

end;

suppose i <> j ; :: thesis: g . j in ((Carrier J) +* i,P) . j

hence g . j in ((Carrier J) +* i,P) . j by A20, FUNCT_7:34; :: thesis: verum

end;

end;

end;

hence x in product ((Carrier J) +* i,P) by A16, A19, CARD_3:def 5; :: thesis: verum

end;

hence (proj J,i) " P = product ((Carrier J) +* i,P) by A3, XBOOLE_0:def 10; :: thesis: verum