theorem :: LANG1:2

for G being non empty DTConstrStr
for s being Symbol of G
for n, n1, n2 being String of G st s ==> n holds
(n1 ^ <*s*>) ^ n2 ==> (n1 ^ n) ^ n2 ;