let H1, H2 be strict multSubmagma of M; :: thesis: ( A c= the carrier of H1 & ( for N being strict multSubmagma of M st A c= the carrier of N holds
H1 is multSubmagma of N ) & A c= the carrier of H2 & ( for N being strict multSubmagma of M st A c= the carrier of N holds
H2 is multSubmagma of N ) implies H1 = H2 )
assume ( A c= the carrier of H1 & ( for N being strict multSubmagma of M st A c= the carrier of N holds
H1 is multSubmagma of N ) & A c= the carrier of H2 & ( for N being strict multSubmagma of M st A c= the carrier of N holds
H2 is multSubmagma of N ) ) ; :: thesis: H1 = H2
then ( H1 is multSubmagma of H2 & H2 is multSubmagma of H1 ) ;
hence H1 = H2 by Th6; :: thesis: verum