let M be multMagma ; for N being multSubmagma of M holds the carrier of N is stable Subset of M
let N be multSubmagma of M; the carrier of N is stable Subset of M
for v, w being Element of M st v in the carrier of N & w in the carrier of N holds
v * w in the carrier of N
proof
let v,
w be
Element of
M;
( v in the carrier of N & w in the carrier of N implies v * w in the carrier of N )
assume A1:
(
v in the
carrier of
N &
w in the
carrier of
N )
;
v * w in the carrier of N
then reconsider v9 =
v,
w9 =
w as
Element of
N ;
A2:
[v,w] in [: the carrier of N, the carrier of N:]
by A1, ZFMISC_1:def 2;
v9 * w9 =
the
multF of
N . [v9,w9]
by BINOP_1:def 1
.=
( the multF of M || the carrier of N) . [v9,w9]
by Def9
.=
( the multF of M | [: the carrier of N, the carrier of N:]) . [v,w]
by REALSET1:def 2
.=
the
multF of
M . [v,w]
by A2, FUNCT_1:49
.=
v * w
by BINOP_1:def 1
;
hence
v * w in the
carrier of
N
by A1;
verum
end;
hence
the carrier of N is stable Subset of M
by Def9, Def10; verum