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;