let X be set ; :: thesis: for v, w being Element of (free_magma X) st not X is empty holds
v * w = [[[(v `1),(w `1)],(v `2)],((length v) + (length w))]
let v, w be Element of (free_magma X); :: thesis: ( not X is empty implies v * w = [[[(v `1),(w `1)],(v `2)],((length v) + (length w))] )
assume A1: not X is empty ; :: thesis: v * w = [[[(v `1),(w `1)],(v `2)],((length v) + (length w))]
then ( length v = v `2 & length w = w `2 ) by Def18;
hence v * w = [[[(v `1),(w `1)],(v `2)],((length v) + (length w))] by A1, Def16; :: thesis: verum