let U be Universe; :: thesis: for G being Group st G is U -element holds
the multF of G is Element of U
let G be Group; :: thesis: ( G is U -element implies the multF of G is Element of U )
assume G is U -element ; :: thesis: the multF of G is Element of U
then reconsider CG = the carrier of G as Element of U ;
[:[:CG,CG:],CG:] is Element of U ;
hence the multF of G is Element of U by CLASSES4:13; :: thesis: verum