let I be non empty set ; :: thesis: for J being non-Empty TopSpace-yielding ManySortedSet of
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 ; :: 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,P) = dom (Carrier J) by FUNCT_7:32
.= I by PARTFUN1:def 4 ;
A2: dom (Carrier J) = 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;
((Carrier J) +* i,P) . i = P by A2, FUNCT_7:33;
then A7: g . i in P by A1, A6;
A8: dom g = dom (Carrier J) by A5, FUNCT_7:32;
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 A9: j in I by PARTFUN1:def 4;
then consider R being 1-sorted such that
A10: R = J . j and
A11: (Carrier J) . j = the carrier of R by PRALG_1:def 13;

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

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

((Carrier J) +* i,P) . i = P by A2, FUNCT_7:33;
then g . j in P by A1, A6, A12;
hence g . j in (Carrier J) . j by A10, A11, A12; :: 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 A1, A6, A9; :: thesis: verum

end;

end;

end;

then A13: g in product (Carrier J) by A8, CARD_3:18;
then A14: g in dom (proj (Carrier J),i) by PRALG_3:def 2;
A15: g in dom (proj J,i) by A13, PRALG_3:def 2;
(proj (Carrier J),i) . g in P by A7, A14, PRALG_3:def 2;
hence x in (proj J,i) " P by A4, A15, 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 A16: x in (proj J,i) " P ; :: thesis: x in product ((Carrier J) +* i,P)
then A17: x in dom (proj (Carrier J),i) by FUNCT_1:def 13;
then x in product (Carrier J) by PRALG_3:def 2;
then consider g being Function such that
A18: x = g and
A19: dom g = dom (Carrier J) and
A20: for y being set st y in dom (Carrier J) holds
g . y in (Carrier J) . y by CARD_3:def 5;
A21: dom g = dom ((Carrier J) +* i,P) by A19, 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 A22: g . j in (Carrier J) . j by A19, A20, A21;

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

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

(proj (Carrier J),i) . x = g . i by A17, A18, PRALG_3:def 2;
then g . i in P by A16, FUNCT_1:def 13;
hence g . j in ((Carrier J) +* i,P) . j by A2, A23, 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 A22, FUNCT_7:34; :: thesis: verum

end;

end;

end;

hence x in product ((Carrier J) +* i,P) by A18, A21, 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