let I be non empty set ; :: thesis: for J being non-Empty TopStruct-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 TopStruct-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 2;
A2: dom ((Carrier J) +* (i,P)) = dom (Carrier J) by FUNCT_7:30
.= I by PARTFUN1:def 2 ;
A3: product ((Carrier J) +* (i,P)) c= (proj (J,i)) " P

proof

let x be object ; :: 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 object 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 object st j in dom (Carrier J) holds
g . j in (Carrier J) . j

proof

let j be object ; :: 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 ;
then A9: ex R being 1-sorted st
( R = J . j & (Carrier J) . j = the carrier of R ) by PRALG_1:def 15;

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:31;
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:32;
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:30;
then A11: g in product (Carrier J) by A7, CARD_3:9;
then A12: g in dom (proj ((Carrier J),i)) by CARD_3:def 16;
((Carrier J) +* (i,P)) . i = P by A1, FUNCT_7:31;
then g . i in P by A2, A6;
then A13: (proj ((Carrier J),i)) . g in P by A12, CARD_3:def 16;
g in dom (proj (J,i)) by A11, CARD_3:def 16;
hence x in (proj (J,i)) " P by A4, A13, FUNCT_1:def 7; :: thesis: verum

end;

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

proof

let x be object ; :: 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 7;
then x in product (Carrier J) ;
then consider g being Function such that
A16: x = g and
A17: dom g = dom (Carrier J) and
A18: for y being object 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:30;
for j being object st j in dom ((Carrier J) +* (i,P)) holds
g . j in ((Carrier J) +* (i,P)) . j

proof

let j be object ; :: 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 16;
then g . i in P by A14, FUNCT_1:def 7;
hence g . j in ((Carrier J) +* (i,P)) . j by A1, A21, FUNCT_7:31; :: 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:32; :: 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; :: thesis: verum