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;

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 )
;

end;