let X be set ; for S being Subset of X holds free_magma S is multSubmagma of free_magma X
let S be Subset of X; free_magma S is multSubmagma of free_magma X
A1:
the carrier of (free_magma S) c= the carrier of (free_magma X)
by Th27;
reconsider A = the carrier of (free_magma S) as set ;
A2:
the multF of (free_magma X) | [:A,A:] = the multF of (free_magma X) || the carrier of (free_magma S)
by REALSET1:def 2;
per cases
( S is empty or not S is empty )
;
suppose A5:
not
S is
empty
;
free_magma S is multSubmagma of free_magma Xthen A6:
dom the
multF of
(free_magma S) = [:A,A:]
by FUNCT_2:def 1;
A7:
not
X is
empty
by A5;
[:A,A:] c= [:(free_magma_carrier X),(free_magma_carrier X):]
by A1, ZFMISC_1:96;
then
[:A,A:] c= dom the
multF of
(free_magma X)
by A7, FUNCT_2:def 1;
then A8:
dom the
multF of
(free_magma S) = dom ( the multF of (free_magma X) || the carrier of (free_magma S))
by A6, A2, RELAT_1:62;
for
z being
object st
z in dom the
multF of
(free_magma S) holds
the
multF of
(free_magma S) . z = ( the multF of (free_magma X) || the carrier of (free_magma S)) . z
proof
let z be
object ;
( z in dom the multF of (free_magma S) implies the multF of (free_magma S) . z = ( the multF of (free_magma X) || the carrier of (free_magma S)) . z )
assume A9:
z in dom the
multF of
(free_magma S)
;
the multF of (free_magma S) . z = ( the multF of (free_magma X) || the carrier of (free_magma S)) . z
then consider x,
y being
object such that A10:
(
x in A &
y in A &
z = [x,y] )
by ZFMISC_1:def 2;
reconsider x =
x,
y =
y as
Element of
free_magma_carrier S by A10;
reconsider n =
x `2 ,
m =
y `2 as
Nat by A5;
reconsider x9 =
x,
y9 =
y as
Element of
free_magma_carrier X by A10, A1;
the
multF of
(free_magma S) . z =
the
multF of
(free_magma S) . (
x,
y)
by A10, BINOP_1:def 1
.=
[[[(x `1),(y `1)],(x `2)],(n + m)]
by A5, Def16
.=
(free_magma_mult X) . (
x9,
y9)
by A7, Def16
.=
the
multF of
(free_magma X) . z
by A10, BINOP_1:def 1
.=
( the multF of (free_magma X) | [:A,A:]) . z
by A9, FUNCT_1:49
;
hence
the
multF of
(free_magma S) . z = ( the multF of (free_magma X) || the carrier of (free_magma S)) . z
by REALSET1:def 2;
verum
end; then
the
multF of
(free_magma S) = the
multF of
(free_magma X) || the
carrier of
(free_magma S)
by A8, FUNCT_1:2;
hence
free_magma S is
multSubmagma of
free_magma X
by A1, Def9;
verum end;