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 by FINSEQ_1:40;
hence ( len p >= 1 & p . 1 = n & p . (len p) = n ) by FINSEQ_1:40; :: 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 that
A1: i >= 1 and
A2: i < len p ; :: thesis: ex a, b being String of G st
( p . i = a & p . (i + 1) = b & a ==> b )
thus ex a, b being String of G st
( p . i = a & p . (i + 1) = b & a ==> b ) by A1, A2, FINSEQ_1:40; :: thesis: verum