let f, g be FinSequence; :: thesis: ( len g > 0 & g is_preposition_of f implies g . 1 = f . 1 )
assume that
A1: len g > 0 and
A2: g is_preposition_of f ; :: thesis: g . 1 = f . 1
A4: len g <= len f by A2, FINSEQ_1:63;
0 + 1 <= len g by A1, NAT_1:13;
hence g . 1 = f . 1 by A2, A4, FINSEQ_6:123; :: thesis: verum