let I be non empty set ; :: thesis: for J being non-Empty TopStruct-yielding ManySortedSet of I
for i being Element of I holds (ProjMap J) . i = proj (J,i)
let J be non-Empty TopStruct-yielding ManySortedSet of I; :: thesis: for i being Element of I holds (ProjMap J) . i = proj (J,i)
let i be Element of I; :: thesis: (ProjMap J) . i = proj (J,i)
dom (Carrier J) = I by PARTFUN1:def 2;
hence (ProjMap J) . i = proj ((Carrier J),i) by Def2
.= proj (J,i) by WAYBEL18:def 4 ;
:: thesis: verum