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 and
A2: n = (n1 ^ n3) ^ n2 and
A3: t ==> n3 ; :: according to LANG1:def 4 :: thesis: 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 ;
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; :: thesis: verum