let G be non empty DTConstrStr ; :: thesis: for n being String of G holds n is_derivable_from n
let n be String of G; :: thesis: n is_derivable_from n
take p = <*n*>; :: according to LANG1:def 5 :: thesis: ( len p >= 1 & p . 1 = n & p . (len p) = n & ( for i being Element of NAT st i >= 1 & i < len p holds
ex a, b being String of G st
( p . i = a & p . (i + 1) = b & a ==> b ) ) )
( len p = 1 & p . 1 = n ) by FINSEQ_1:57;
hence ( len p >= 1 & p . 1 = n & p . (len p) = n ) ; :: thesis: for i being Element of NAT st i >= 1 & i < len p holds
ex a, b being String of G st
( p . i = a & p . (i + 1) = b & a ==> b )
let i be Element of NAT ; :: thesis: ( i >= 1 & i < len p implies ex a, b being String of G st
( p . i = a & p . (i + 1) = b & a ==> b ) )
assume ( i >= 1 & i < len p ) ; :: thesis: ex a, b being String of G st
( p . i = a & p . (i + 1) = b & a ==> b )
hence ex a, b being String of G st
( p . i = a & p . (i + 1) = b & a ==> b ) by FINSEQ_1:57; :: thesis: verum