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;