set Y = RealPoset [.0,1.];
the carrier of (RealPoset [.0,1.]) = [.0,1.] by LFUZZY_0:def 3;
hence the carrier of ((RealPoset [.0,1.]) |^ [.0,1.]) = Funcs ([.0,1.],[.0,1.]) by YELLOW_1:28; :: thesis: verum