let X be non empty set ; for A being Subset of (free_magma X) st A = (canon_image (X,1)) .: X holds
free_magma X = the_submagma_generated_by A
let A be Subset of (free_magma X); ( A = (canon_image (X,1)) .: X implies free_magma X = the_submagma_generated_by A )
set N = the_submagma_generated_by A;
assume A1:
A = (canon_image (X,1)) .: X
; free_magma X = the_submagma_generated_by A
per cases
( A is empty or not A is empty )
;
suppose A4:
not
A is
empty
;
free_magma X = the_submagma_generated_by AA5:
the
carrier of
(the_submagma_generated_by A) c= the
carrier of
(free_magma X)
by Def9;
for
x being
object st
x in the
carrier of
(free_magma X) holds
x in the
carrier of
(the_submagma_generated_by A)
proof
let x be
object ;
( x in the carrier of (free_magma X) implies x in the carrier of (the_submagma_generated_by A) )
assume A6:
x in the
carrier of
(free_magma X)
;
x in the carrier of (the_submagma_generated_by A)
defpred S1[
Nat]
means for
v being
Element of
(free_magma X) st
length v = $1 holds
v in the
carrier of
(the_submagma_generated_by A);
A7:
for
k being
Nat st ( for
n being
Nat st
n < k holds
S1[
n] ) holds
S1[
k]
proof
let k be
Nat;
( ( for n being Nat st n < k holds
S1[n] ) implies S1[k] )
assume A8:
for
n being
Nat st
n < k holds
S1[
n]
;
S1[k]
(
k = 0 or
k + 1
> 0 + 1 )
by XREAL_1:6;
then
(
k = 0 or
k >= 1 )
by NAT_1:13;
then
(
k = 0 or
k = 1 or
k > 1 )
by XXREAL_0:1;
then A9:
(
k = 0 or
k = 1 or
k + 1
> 1
+ 1 )
by XREAL_1:6;
per cases
( k = 0 or k = 1 or k >= 2 )
by A9, NAT_1:13;
suppose A14:
k >= 2
;
S1[k]
for
v being
Element of
(free_magma X) st
length v = k holds
v in the
carrier of
(the_submagma_generated_by A)
proof
let v be
Element of
(free_magma X);
( length v = k implies v in the carrier of (the_submagma_generated_by A) )
assume A15:
length v = k
;
v in the carrier of (the_submagma_generated_by A)
then consider v1,
v2 being
Element of
(free_magma X) such that A16:
(
v = v1 * v2 &
length v1 < length v &
length v2 < length v )
by A14, Th34;
A17:
v1 in the
carrier of
(the_submagma_generated_by A)
by A8, A15, A16;
reconsider v19 =
v1 as
Element of
(the_submagma_generated_by A) by A8, A15, A16;
A18:
v2 in the
carrier of
(the_submagma_generated_by A)
by A8, A15, A16;
reconsider v29 =
v2 as
Element of
(the_submagma_generated_by A) by A8, A15, A16;
not
the_submagma_generated_by A is
empty
by A4, Th14;
then A19:
the
carrier of
(the_submagma_generated_by A) <> {}
;
A20:
[v1,v2] in [: the carrier of (the_submagma_generated_by A), the carrier of (the_submagma_generated_by A):]
by A17, A18, ZFMISC_1:87;
v19 * v29 =
the
multF of
(the_submagma_generated_by A) . [v19,v29]
by BINOP_1:def 1
.=
( the multF of (free_magma X) || the carrier of (the_submagma_generated_by A)) . [v1,v2]
by Def9
.=
( the multF of (free_magma X) | [: the carrier of (the_submagma_generated_by A), the carrier of (the_submagma_generated_by A):]) . [v1,v2]
by REALSET1:def 2
.=
the
multF of
(free_magma X) . [v1,v2]
by A20, FUNCT_1:49
.=
v1 * v2
by BINOP_1:def 1
;
hence
v in the
carrier of
(the_submagma_generated_by A)
by A16, A19;
verum
end; hence
S1[
k]
;
verum
end;
A21:
for
n being
Nat holds
S1[
n]
from NAT_1:sch 4(A7);
reconsider v =
x as
Element of
(free_magma X) by A6;
reconsider k =
length v as
Nat ;
S1[
k]
by A21;
hence
x in the
carrier of
(the_submagma_generated_by A)
;
verum
end; then
the
carrier of
(free_magma X) c= the
carrier of
(the_submagma_generated_by A)
;
then
the
carrier of
(free_magma X) = the
carrier of
(the_submagma_generated_by A)
by A5, XBOOLE_0:def 10;
hence
free_magma X = the_submagma_generated_by A
by Th7;
verum end;