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 )
given n1, n2, n3 being String of G, t being Symbol of G such that A1: ( <*s*> = (n1 ^ <*t*>) ^ n2 & n = (n1 ^ n3) ^ n2 & t ==> n3 ) ; :: according to LANG1:def 4 :: thesis: s ==> n
( len <*s*> = 1 & len <*t*> = 1 & len (n1 ^ <*t*>) = (len n1) + (len <*t*>) & len <*s*> = (len (n1 ^ <*t*>)) + (len n2) ) by A1, FINSEQ_1:35, FINSEQ_1:57;
then 1 + 0 = 1 + ((len n1) + (len n2)) ;
then ( len n1 = 0 & len n2 = 0 ) by NAT_1:7;
then ( n1 = {} & n2 = {} & {} ^ <*t*> = <*t*> & <*t*> ^ {} = <*t*> & {} ^ n3 = n3 & n3 ^ {} = n3 & <*s*> . 1 = s & <*t*> . 1 = t ) by FINSEQ_1:47, FINSEQ_1:57;
hence s ==> n by A1; :: thesis: verum