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

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