per cases ( G is unital or not G is unital ) ;

suppose G is unital ; :: thesis: not .: (G,A) is empty

then .: (G,A) = multLoopStr(# (Funcs (A, the carrier of G)),(( the multF of G, the carrier of G) .: A),(A --> (the_unity_wrt the multF of G)) #) by Def3;
hence not the carrier of (.: (G,A)) is empty ; :: according to STRUCT_0:def 1 :: thesis: verum

end;

suppose not G is unital ; :: thesis: not .: (G,A) is empty

then .: (G,A) = multMagma(# (Funcs (A, the carrier of G)),(( the multF of G, the carrier of G) .: A) #) by Def3;
hence not the carrier of (.: (G,A)) is empty ; :: according to STRUCT_0:def 1 :: thesis: verum

end;

end;