:: deftheorem Def5 defines Pt2FinSeq MEASUR14:def 5 :
for m being non zero Nat
for X being non-empty b₁ -element FinSequence
for b₃ being b₁ -element FinSequence holds
( b₃ = Pt2FinSeq X iff ( ex id1 being Function of (CarProduct (SubFin (X,1))),(product (SubFin (X,1))) st
( b₃ . 1 = id1 & id1 is bijective & ( for x being object st x in CarProduct (SubFin (X,1)) holds
id1 . x = <*x*> ) ) & ( for i being non zero Nat st i < m holds
ex Fi being Function of (CarProduct (SubFin (X,i))),(product (SubFin (X,i))) ex IK being Function of [:(CarProduct (SubFin (X,i))),(ElmFin (X,(i + 1))):],(product (SubFin (X,(i + 1)))) st
( Fi = b₃ . i & IK = b₃ . (i + 1) & Fi is bijective & IK is bijective & ( for x, y being object st x in CarProduct (SubFin (X,i)) & y in ElmFin (X,(i + 1)) holds
ex s being FinSequence st
( Fi . x = s & IK . (x,y) = s ^ <*y*> ) ) ) ) ) );