let G be non empty DTConstrStr ; :: thesis: for s being Element of G
for p being FinSequence st s ==> p holds
p is FinSequence of the carrier of G
let s be Element of G; :: thesis: for p being FinSequence st s ==> p holds
p is FinSequence of the carrier of G
let p be FinSequence; :: thesis: ( s ==> p implies p is FinSequence of the carrier of G )
assume s ==> p ; :: thesis: p is FinSequence of the carrier of G
then [s,p] in the Rules of G ;
then p in the carrier of G * by ZFMISC_1:87;
hence p is FinSequence of the carrier of G by FINSEQ_1:def 11; :: thesis: verum