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