:: deftheorem Def1 defines || MESFUN9C:def 1 :
for X, Y being set
for F being Functional_Sequence of X,Y
for D being set
for b₅ being Functional_Sequence of X,Y holds
( b₅ = F || D iff for n being Nat holds b₅ . n = (F . n) | D );