the carrier of (V *') is functional by Th1;
hence V *' is constituted-Functions by MONOID_0:80; :: thesis: verum