:: deftheorem Def3 defines ExtendRel FINSEQ_3:def 3 :
for D being non empty set
for R being Relation of D
for b₃ being Relation of (D *) holds
( b₃ = ExtendRel R iff for x, y being FinSequence of D holds
( [x,y] in b₃ iff ( len x = len y & ( for n being Nat st n in dom x holds
[(x . n),(y . n)] in R ) ) ) );