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 3;
per cases
( S is empty or not S is empty )
;
suppose A5:
not
S is
empty
;
free_magma S is multSubmagma of free_magma XA6:
dom the
multF of
(free_magma S) = [:A,A:]
by A5, 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:119;
then A8:
[:A,A:] c= dom the
multF of
(free_magma X)
by A7, FUNCT_2:def 1;
A9:
dom the
multF of
(free_magma S) = dom (the multF of (free_magma X) || the carrier of (free_magma S))
by A6, A2, A8, RELAT_1:91;
A10:
for
z being
set 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
set ;
( 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 A11:
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
consider x,
y being
set such that A12:
(
x in A &
y in A &
z = [x,y] )
by A11, ZFMISC_1:def 2;
reconsider x =
x,
y =
y as
Element of
free_magma_carrier S by A12;
reconsider n =
x `2 ,
m =
y `2 as
natural number by A5;
reconsider x9 =
x,
y9 =
y as
Element of
free_magma_carrier X by A12, A1;
the
multF of
(free_magma S) . z =
the
multF of
(free_magma S) . x,
y
by A12, BINOP_1:def 1
.=
[[[(x `1 ),(y `1 )],(x `2 )],(n + m)]
by A5, Def17
.=
(free_magma_mult X) . x9,
y9
by A7, Def17
.=
the
multF of
(free_magma X) . z
by A12, BINOP_1:def 1
.=
(the multF of (free_magma X) | [:A,A:]) . z
by A11, FUNCT_1:72
;
hence
the
multF of
(free_magma S) . z = (the multF of (free_magma X) || the carrier of (free_magma S)) . z
by REALSET1:def 3;
verum
end;
the
multF of
(free_magma S) = the
multF of
(free_magma X) || the
carrier of
(free_magma S)
by A9, A10, FUNCT_1:9;
hence
free_magma S is
multSubmagma of
free_magma X
by A1, Def10;
verum end;