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, Def10;
then A4: the carrier of N = the carrier of K by XBOOLE_0:def 10;
the multF of N = the multF of K || the carrier of N by A1, Def10
.= (the multF of N || the carrier of K) || the carrier of N by A2, Def10
.= (the multF of N | [:the carrier of K,the carrier of K:]) || the carrier of N by REALSET1:def 3
.= (the multF of N | [:the carrier of K,the carrier of K:]) | [:the carrier of N,the carrier of N:] by REALSET1:def 3
.= the multF of N | [:the carrier of K,the carrier of K:] by A4, RELAT_1:101
.= the multF of N || the carrier of K by REALSET1:def 3
.= the multF of K by A2, Def10 ;
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