let G1 be non empty associative multMagma ; :: thesis: <*G1*> is associative multMagma-Family of {1}
reconsider A = <*G1*> as multMagma-Family of {1} ;
A is associative

proof

let x be Element of {1}; :: according to GROUP_7:def 7 :: thesis: A . x is associative
x = 1 by TARSKI:def 1;
hence A . x is associative ; :: thesis: verum

end;

hence <*G1*> is associative multMagma-Family of {1} ; :: thesis: verum