:: deftheorem Def1 defines pr1 PRALG_1:def 1 :
for A, B being non empty set
for h1 being FinSequence of [:A,B:]
for b₄ being FinSequence of A holds
( b₄ = pr1 h1 iff ( len b₄ = len h1 & ( for n being Nat st n in dom b₄ holds
b₄ . n = (h1 . n) `1 ) ) );