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, XTUPLE_0:1;
then A4: ( [(v1 `1),(v2 `1)] = [(w1 `1),(w2 `1)] & v1 `2 = w1 `2 ) by XTUPLE_0:1;
length v1 = v1 `2 by A2, Def18
.= length w1 by A2, A4, Def18 ;
then v2 `2 = length w2 by A2, A3, Def18;
then A5: v2 `2 = w2 `2 by A2, Def18;
thus v1 = [(v1 `1),(v1 `2)] by A2, Th32
.= [(w1 `1),(w1 `2)] by A4, XTUPLE_0:1
.= w1 by A2, Th32 ; :: thesis: v2 = w2
thus v2 = [(v2 `1),(v2 `2)] by A2, Th32
.= [(w2 `1),(w2 `2)] by A5, A4, XTUPLE_0:1
.= 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 1;
hence ( v1 = w1 & v2 = w2 ) ; :: thesis: verum

end;

end;