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

end;

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;hence not the carrier of (.: (G,A)) is empty ; :: according to STRUCT_0:def 1 :: thesis: verum