C is Category-like ;
then consider y1, y2 being set , y3, y4 being Function of y2,y1, y5 being PartFunc of [:y2,y2:],y2 such that
A1: ( y1 = C `1 & y2 = C `2 & y3 = C `3 & y4 = C `4 & y5 = C `5 & CatStr(# y1,y2,y3,y4,y5 #) is Category ) ;
reconsider C = CatStr(# y1,y2,y3,y4,y5 #) as Category by A1;
thus ex b<sub>1</sub> being strict Category ex y1, y2 being set ex y3, y4 being Function of y2,y1 ex y5 being PartFunc of [:y2,y2:],y2 st
( y1 = C `1 & y2 = C `2 & y3 = C `3 & y4 = C `4 & y5 = C `5 & b₁ = CatStr(# y1,y2,y3,y4,y5 #) ) by A1; :: thesis: verum