let G be non empty DTConstrStr ; for s being Symbol of G
for n being String of G st <*s*> ==> n holds
s ==> n
let s be Symbol of G; for n being String of G st <*s*> ==> n holds
s ==> n
let n be String of G; ( <*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
and
A2:
n = (n1 ^ n3) ^ n2
and
A3:
t ==> n3
; LANG1:def 4 s ==> n
A4:
len <*t*> = 1
by FINSEQ_1:40;
A5:
len (n1 ^ <*t*>) = (len n1) + (len <*t*>)
by FINSEQ_1:22;
len <*s*> = (len (n1 ^ <*t*>)) + (len n2)
by A1, FINSEQ_1:22;
then A6:
1 + 0 = 1 + ((len n1) + (len n2))
by A4, A5, FINSEQ_1:40;
then A7:
n2 = {}
by NAT_1:7;
A8:
n3 ^ {} = n3
by FINSEQ_1:34;
A9:
{} ^ n3 = n3
by FINSEQ_1:34;
A10:
<*s*> . 1 = s
by FINSEQ_1:40;
A11:
<*t*> ^ {} = <*t*>
by FINSEQ_1:34;
A12:
{} ^ <*t*> = <*t*>
by FINSEQ_1:34;
n1 = {}
by A6, NAT_1:7;
hence
s ==> n
by A1, A2, A3, A7, A12, A11, A9, A8, A10, FINSEQ_1:40; verum