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 #)

A2: the multF of M = the multF of M | [: the carrier of M, the carrier of M:]
.= the multF of M || the carrier of M by REALSET1:def 2 ;
then reconsider M9 = M as multSubmagma of M by Def9;
the multF of M9 = the multF of N || the carrier of M9 by A1, A2, Def9;
then M9 is multSubmagma of N by A1, Def9;
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;