let G be non empty DTConstrStr ; :: thesis: for s being Symbol of G
for n, n1, n2 being String of G st s ==> n holds
(n1 ^ <*s*>) ^ n2 ==> (n1 ^ n) ^ n2
let s be Symbol of G; :: thesis: for n, n1, n2 being String of G st s ==> n holds
(n1 ^ <*s*>) ^ n2 ==> (n1 ^ n) ^ n2
let n, n1, n2 be String of G; :: thesis: ( s ==> n implies (n1 ^ <*s*>) ^ n2 ==> (n1 ^ n) ^ n2 )
assume A1: s ==> n ; :: thesis: (n1 ^ <*s*>) ^ n2 ==> (n1 ^ n) ^ n2
take n1 ; :: according to LANG1:def 4 :: thesis: ex n2, n3 being String of G ex s being Symbol of G st
( (n1 ^ <*s*>) ^ n2 = (n1 ^ <*s*>) ^ n2 & (n1 ^ n) ^ n2 = (n1 ^ n3) ^ n2 & s ==> n3 )
take n2 ; :: thesis: ex n3 being String of G ex s being Symbol of G st
( (n1 ^ <*s*>) ^ n2 = (n1 ^ <*s*>) ^ n2 & (n1 ^ n) ^ n2 = (n1 ^ n3) ^ n2 & s ==> n3 )
take n ; :: thesis: ex s being Symbol of G st
( (n1 ^ <*s*>) ^ n2 = (n1 ^ <*s*>) ^ n2 & (n1 ^ n) ^ n2 = (n1 ^ n) ^ n2 & s ==> n )
take s ; :: thesis: ( (n1 ^ <*s*>) ^ n2 = (n1 ^ <*s*>) ^ n2 & (n1 ^ n) ^ n2 = (n1 ^ n) ^ n2 & s ==> n )
thus ( (n1 ^ <*s*>) ^ n2 = (n1 ^ <*s*>) ^ n2 & (n1 ^ n) ^ n2 = (n1 ^ n) ^ n2 & s ==> n ) by A1; :: thesis: verum