let X be set ; :: thesis: X = { (w `1) where w is Element of (free_magma X) : length w = 1 }
for x being object holds
( x in X iff x in { (w `1) where w is Element of (free_magma X) : length w = 1 } )

proof

let x be object ; :: thesis: ( x in X iff x in { (w `1) where w is Element of (free_magma X) : length w = 1 } )

hereby :: thesis: ( x in { (w `1) where w is Element of (free_magma X) : length w = 1 } implies x in X )

assume A1: x in X ; :: thesis: x in { (w `1) where w is Element of (free_magma X) : length w = 1 }
then A2: x in free_magma (X,1) by Def13;
1 in {1} by TARSKI:def 1;
then A3: [x,1] in [:(free_magma (X,1)),{1}:] by A2, ZFMISC_1:def 2;
[:(free_magma (X,1)),{1}:] c= free_magma_carrier X by Lm1;
then reconsider w9 = [x,1] as Element of (free_magma X) by A3;
1 = [x,1] `2 ;
then A4: length w9 = 1 by A1, Def18;
x = [x,1] `1 ;
hence x in { (w `1) where w is Element of (free_magma X) : length w = 1 } by A4; :: thesis: verum

end;

assume x in { (w `1) where w is Element of (free_magma X) : length w = 1 } ; :: thesis: x in X
then consider w being Element of (free_magma X) such that
A5: ( x = w `1 & length w = 1 ) ;
A6: w `2 = 1 by A5, Def18;

per cases ( not X is empty or X is empty ) ;

suppose not X is empty ; :: thesis: x in X

then w in [:(free_magma (X,1)),{1}:] by A6, Th25;
then w in [:X,{1}:] by Def13;
hence x in X by A5, MCART_1:10; :: thesis: verum

end;

suppose X is empty ; :: thesis: x in X

hence x in X by A5, Def18; :: thesis: verum

end;

end;

end;

hence X = { (w `1) where w is Element of (free_magma X) : length w = 1 } by TARSKI:2; :: thesis: verum