let M be multMagma ; :: thesis: for N, K being multSubmagma of M st N is multSubmagma of K & K is multSubmagma of N holds
multMagma(# the carrier of N, the multF of N #) = multMagma(# the carrier of K, the multF of K #)
let N, K be multSubmagma of M; :: thesis: ( N is multSubmagma of K & K is multSubmagma of N implies multMagma(# the carrier of N, the multF of N #) = multMagma(# the carrier of K, the multF of K #) )
assume that
A1: N is multSubmagma of K and
A2: K is multSubmagma of N ; :: thesis: multMagma(# the carrier of N, the multF of N #) = multMagma(# the carrier of K, the multF of K #)
set A = the carrier of N;
set B = the carrier of K;
set f = the multF of N;
set g = the multF of K;
A3: ( the carrier of N c= the carrier of K & the carrier of K c= the carrier of N ) by A1, A2, Def9;
the multF of N = the multF of K || the carrier of N by A1, Def9
.= ( the multF of N || the carrier of K) || the carrier of N by A2, Def9
.= ( the multF of N | [: the carrier of K, the carrier of K:]) || the carrier of N by REALSET1:def 2
.= ( the multF of N | [: the carrier of K, the carrier of K:]) | [: the carrier of N, the carrier of N:] by REALSET1:def 2
.= the multF of N || the carrier of K by REALSET1:def 2
.= the multF of K by A2, Def9 ;
hence multMagma(# the carrier of N, the multF of N #) = multMagma(# the carrier of K, the multF of K #) by A3, XBOOLE_0:def 10; :: thesis: verum