let X be set ; :: thesis: for v, w being Element of (free_magma X) holds length (v * w) = (length v) + (length w)
let v, w be Element of (free_magma X); :: thesis: length (v * w) = (length v) + (length w)
set vw = v * w;

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

suppose A1: not X is empty ; :: thesis: length (v * w) = (length v) + (length w)

then A2: v * w = [[[(v `1),(w `1)],(v `2)],((length v) + (length w))] by Th31;
thus length (v * w) = (v * w) `2 by A1, Def19
.= (length v) + (length w) by A2, MCART_1:def 2 ; :: thesis: verum

end;

suppose A3: X is empty ; :: thesis: length (v * w) = (length v) + (length w)

hence length (v * w) = 0 by Def19
.= (length v) + 0 by A3, Def19
.= (length v) + (length w) by A3, Def19 ;
:: thesis: verum

end;

end;