theorem :: FOMODEL0:38

for U being non empty set holds (U -concatenation) .: (id (1 -tuples_on U)) = { <*u,u*> where u is Element of U : verum }