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 that
A1: len g > 0 and
A2: f is_preposition_of ; :: thesis: g . 1 = f . 1
A3: mid f,1,(len g) = g by A1, A2, Def8;
A4: len g <= len f by A2, FINSEQ_1:84;
0 + 1 <= len g by A1, NAT_1:13;
hence g . 1 = f . 1 by A3, A4, JORDAN3:32; :: thesis: verum