let X, Y be set ; :: thesis: ( X c= Y implies free_magma_carrier X c= free_magma_carrier Y )
assume A1: X c= Y ; :: thesis: free_magma_carrier X c= free_magma_carrier Y

per cases ( X = {} or X <> {} ) ;

suppose X = {} ; :: thesis: free_magma_carrier X c= free_magma_carrier Y

then free_magma_carrier X = {} ;
hence free_magma_carrier X c= free_magma_carrier Y ; :: thesis: verum

end;

suppose A2: X <> {} ; :: thesis: free_magma_carrier X c= free_magma_carrier Y

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in free_magma_carrier X or x in free_magma_carrier Y )
assume A3: x in free_magma_carrier X ; :: thesis: x in free_magma_carrier Y
reconsider 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; :: thesis: verum

end;

end;