let M be multMagma ; :: thesis: for N being multSubmagma of M st the carrier of N = the carrier of M holds
multMagma(# the carrier of N,the multF of N #) = multMagma(# the carrier of M,the multF of M #)
let N be multSubmagma of M; :: thesis: ( the carrier of N = the carrier of M implies multMagma(# the carrier of N,the multF of N #) = multMagma(# the carrier of M,the multF of M #) )
assume A1: the carrier of N = the carrier of M ; :: thesis: multMagma(# the carrier of N,the multF of N #) = multMagma(# the carrier of M,the multF of M #)

per cases ( the carrier of M = {} or the carrier of M <> {} ) ;

suppose the carrier of M = {} ; :: thesis: multMagma(# the carrier of N,the multF of N #) = multMagma(# the carrier of M,the multF of M #)

hence multMagma(# the carrier of N,the multF of N #) = multMagma(# the carrier of M,the multF of M #) by A1; :: thesis: verum

end;

suppose the carrier of M <> {} ; :: thesis: multMagma(# the carrier of N,the multF of N #) = multMagma(# the carrier of M,the multF of M #)

then dom the multF of M = [:the carrier of M,the carrier of M:] by FUNCT_2:def 1;
then A2: the multF of M = the multF of M | [:the carrier of M,the carrier of M:] by RELAT_1:98
.= the multF of M || the carrier of M by REALSET1:def 3 ;
then reconsider M9 = M as multSubmagma of M by Def10;
the multF of M9 = the multF of N || the carrier of M9 by A1, A2, Def10;
then M9 is multSubmagma of N by A1, Def10;
hence multMagma(# the carrier of N,the multF of N #) = multMagma(# the carrier of M,the multF of M #) by Th6; :: thesis: verum

end;

end;