let D be non empty set ; :: thesis: for p, q being FinSequence of D
for i being Element of NAT st p c= q & 1 <= i & i <= len p holds
q . i = p . i
let p, q be FinSequence of D; :: thesis: for i being Element of NAT st p c= q & 1 <= i & i <= len p holds
q . i = p . i
let i be Element of NAT ; :: thesis: ( p c= q & 1 <= i & i <= len p implies q . i = p . i )
assume p c= q ; :: thesis: ( not 1 <= i or not i <= len p or q . i = p . i )
then A1: ex p9 being FinSequence of D st p ^ p9 = q by Th80;
assume ( 1 <= i & i <= len p ) ; :: thesis: q . i = p . i
hence q . i = p . i by A1, FINSEQ_1:64; :: thesis: verum