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 v * w = [[[(v `1),(w `1)],(v `2)],((length v) + (length w))] by Th31;
hence length (v * w) = [[[(v `1),(w `1)],(v `2)],((length v) + (length w))] `2 by A1, Def18
.= (length v) + (length w) ;
:: thesis: verum

end;

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

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

end;

end;