let X be non empty set ; :: thesis: for v, w being Element of free_magma_carrier X holds [[[(v `1),(w `1)],(v `2)],((v `2) + (w `2))] is Element of free_magma_carrier X
let v, w be Element of free_magma_carrier X; :: thesis: [[[(v `1),(w `1)],(v `2)],((v `2) + (w `2))] is Element of free_magma_carrier X
v in [:(free_magma (X,(v `2))),{(v `2)}:] by Th25;
then A1: v `1 in free_magma (X,(v `2)) by MCART_1:10;
w in [:(free_magma (X,(w `2))),{(w `2)}:] by Th25;
then w `1 in free_magma (X,(w `2)) by MCART_1:10;
then A2: [[(v `1),(w `1)],(v `2)] in free_magma (X,((v `2) + (w `2))) by A1, Th22;
A3: (v `2) + (w `2) in {((v `2) + (w `2))} by TARSKI:def 1;
set z = [[[(v `1),(w `1)],(v `2)],((v `2) + (w `2))];
A4: [[[(v `1),(w `1)],(v `2)],((v `2) + (w `2))] `1 in free_magma (X,((v `2) + (w `2))) by A2;
[[[(v `1),(w `1)],(v `2)],((v `2) + (w `2))] `2 in {((v `2) + (w `2))} by A3;
then A5: [[[(v `1),(w `1)],(v `2)],((v `2) + (w `2))] in [:(free_magma (X,((v `2) + (w `2)))),{((v `2) + (w `2))}:] by A4, ZFMISC_1:def 2;
[:(free_magma (X,((v `2) + (w `2)))),{((v `2) + (w `2))}:] c= free_magma_carrier X by Lm1;
hence [[[(v `1),(w `1)],(v `2)],((v `2) + (w `2))] is Element of free_magma_carrier X by A5; :: thesis: verum