let C be strict Category; :: thesis: SetToCat (CatToSet C) = C
set C2 = CatToSet C;
ex y1, y2 being set ex y3, y4 being Function of y2,y1 ex y5 being PartFunc of [:y2,y2:],y2 st
( y1 = (CatToSet C) `1 & y2 = (CatToSet C) `2 & y3 = (CatToSet C) `3 & y4 = (CatToSet C) `4 & y5 = (CatToSet C) `5 & SetToCat (CatToSet C) = CatStr(# y1,y2,y3,y4,y5 #) ) by Def31;
hence SetToCat (CatToSet C) = C ; :: thesis: verum