let X, Y be set ; ( X c= Y implies free_magma_carrier X c= free_magma_carrier Y )
assume A1:
X c= Y
; free_magma_carrier X c= free_magma_carrier Y
per cases
( X = {} or X <> {} )
;
suppose A2:
X <> {}
;
free_magma_carrier X c= free_magma_carrier Ylet x be
object ;
TARSKI:def 3 ( not x in free_magma_carrier X or x in free_magma_carrier Y )assume A3:
x in free_magma_carrier X
;
x in free_magma_carrier Yreconsider X9 =
X as non
empty set by A2;
reconsider w =
x as
Element of
free_magma_carrier X9 by A3;
A4:
w in [:(free_magma (X9,(w `2))),{(w `2)}:]
by Th25;
then A5:
(
w `1 in free_magma (
X9,
(w `2)) &
w `2 in {(w `2)} )
by MCART_1:10;
reconsider Y9 =
Y as non
empty set by A2, A1;
A6:
free_magma (
X9,
(w `2))
c= free_magma (
Y9,
(w `2))
by A1, Th23;
w = [(w `1),(w `2)]
by A4, MCART_1:21;
then A7:
w in [:(free_magma (Y9,(w `2))),{(w `2)}:]
by A6, A5, ZFMISC_1:def 2;
[:(free_magma (Y9,(w `2))),{(w `2)}:] c= free_magma_carrier Y9
by Lm1;
hence
x in free_magma_carrier Y
by A7;
verum end; end;