:: deftheorem DefSK defines .|. RUSUB_6:def 2 :
for V being non empty UNITSTR
for u being Point of V
for x being FinSequence of V
for b₄ being FinSequence of REAL holds
( b₄ = u .|. x iff ( len b₄ = len x & ( for i being Nat st 1 <= i & i <= len x holds
b₄ . i = u .|. (x /. i) ) ) );