:: deftheorem Def10 defines FinSeqM ROUGHS_1:def 10 :
for A being finite Tolerance_Space
for X being FinSequence of bool the carrier of A
for x being Element of A
for b₄ being FinSequence of REAL holds
( b₄ = FinSeqM (x,X) iff ( dom b₄ = dom X & ( for n being Nat st n in dom X holds
b₄ . n = (MemberFunc ((X . n),A)) . x ) ) );