:: deftheorem DEF3 defines * ANPROJ_8:def 3 :
for p being FinSequence of 1 -tuples_on REAL
for a being Real st len p = 3 holds
for b₃ being FinSequence of 1 -tuples_on REAL holds
( b₃ = a * p iff ex p1, p2, p3 being Real st
( p1 = (p . 1) . 1 & p2 = (p . 2) . 1 & p3 = (p . 3) . 1 & b₃ = <*<*(a * p1)*>,<*(a * p2)*>,<*(a * p3)*>*> ) );