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, MCART_1:def 1;
[[[(v `1 ),(w `1 )],(v `2 )],((v `2 ) + (w `2 ))] `2 in {((v `2 ) + (w `2 ))} by A3, MCART_1:def 2;
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, MCART_1:11;
[:(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