let f1, f2 be FinSubsequence; :: thesis: ( dom f1 = { (i + k) where k is Element of NAT : k in dom p } & ( for j being Nat st j in dom p holds
f1 . (i + j) = p . j ) & dom f2 = { (i + k) where k is Element of NAT : k in dom p } & ( for j being Nat st j in dom p holds
f2 . (i + j) = p . j ) implies f1 = f2 )
assume that
A14: dom f1 = { (i + k) where k is Element of NAT : k in dom p } and
A15: for j being Nat st j in dom p holds
f1 . (i + j) = p . j and
A16: dom f2 = { (i + k) where k is Element of NAT : k in dom p } and
A17: for j being Nat st j in dom p holds
f2 . (i + j) = p . j ; :: thesis: f1 = f2

now

let x be set ; :: thesis: ( x in { (i + k) where k is Element of NAT : k in dom p } implies f1 . x = f2 . x )
assume x in { (i + k) where k is Element of NAT : k in dom p } ; :: thesis: f1 . x = f2 . x
then consider k being Element of NAT such that
A18: x = i + k and
A19: k in dom p ;
thus f1 . x = p . k by A15, A18, A19
.= f2 . x by A17, A18, A19 ; :: thesis: verum

end;

hence f1 = f2 by A14, A16, FUNCT_1:2; :: thesis: verum