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