let M be multMagma ; 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; ( 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
; 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, the carrier of K:]
.=
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; verum