let D be non empty set ; :: thesis: for f, g being FinSequence of D st len g > 0 & f is_preposition_of holds
g . 1 = f . 1
let f, g be FinSequence of D; :: thesis: ( len g > 0 & f is_preposition_of implies g . 1 = f . 1 )
assume A1: ( len g > 0 & f is_preposition_of ) ; :: thesis: g . 1 = f . 1
then A2: ( 1 <= len f & mid f,1,(len g) = g ) by Def8;
A3: len g <= len f by A1, FINSEQ_1:84;
0 + 1 <= len g by A1, NAT_1:13;
hence g . 1 = f . 1 by A2, A3, JORDAN3:32; :: thesis: verum