let X be set ; :: thesis: for v1, v2, w1, w2 being Element of (free_magma X) st v1 * v2 = w1 * w2 holds
( v1 = w1 & v2 = w2 )
let v1, v2, w1, w2 be Element of (free_magma X); :: thesis: ( v1 * v2 = w1 * w2 implies ( v1 = w1 & v2 = w2 ) )
assume A1: v1 * v2 = w1 * w2 ; :: thesis: ( v1 = w1 & v2 = w2 )

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

suppose A2: not X is empty ; :: thesis: ( v1 = w1 & v2 = w2 )

then ( v1 * v2 = [[[(v1 `1 ),(v2 `1 )],(v1 `2 )],((length v1) + (length v2))] & w1 * w2 = [[[(w1 `1 ),(w2 `1 )],(w1 `2 )],((length w1) + (length w2))] ) by Th31;
then A3: ( [[(v1 `1 ),(v2 `1 )],(v1 `2 )] = [[(w1 `1 ),(w2 `1 )],(w1 `2 )] & (length v1) + (length v2) = (length w1) + (length w2) ) by A1, ZFMISC_1:33;
then A4: ( [(v1 `1 ),(v2 `1 )] = [(w1 `1 ),(w2 `1 )] & v1 `2 = w1 `2 ) by ZFMISC_1:33;
length v1 = v1 `2 by A2, Def19
.= length w1 by A2, A4, Def19 ;
then v2 `2 = length w2 by A2, A3, Def19;
then A5: v2 `2 = w2 `2 by A2, Def19;
thus v1 = [(v1 `1 ),(v1 `2 )] by A2, Th32
.= [(w1 `1 ),(w1 `2 )] by A4, ZFMISC_1:33
.= w1 by A2, Th32 ; :: thesis: v2 = w2
thus v2 = [(v2 `1 ),(v2 `2 )] by A2, Th32
.= [(w2 `1 ),(w2 `2 )] by A5, A4, ZFMISC_1:33
.= w2 by A2, Th32 ; :: thesis: verum

end;

suppose X is empty ; :: thesis: ( v1 = w1 & v2 = w2 )

then ( v1 = {} & w1 = {} & v2 = {} & w2 = {} ) by SUBSET_1:def 2;
hence ( v1 = w1 & v2 = w2 ) ; :: thesis: verum

end;

end;