:: deftheorem Def3 defines [[: PRALG_1:def 3 :
for A, B being non empty set
for f1 being non empty homogeneous quasi_total PartFunc of (A *),A
for f2 being non empty homogeneous quasi_total PartFunc of (B *),B st arity f1 = arity f2 holds
for b₅ being non empty homogeneous quasi_total PartFunc of ([:A,B:] *),[:A,B:] holds
( b₅ = [[:f1,f2:]] iff ( dom b₅ = (arity f1) -tuples_on [:A,B:] & ( for h being FinSequence of [:A,B:] st h in dom b₅ holds
b₅ . h = [(f1 . (pr1 h)),(f2 . (pr2 h))] ) ) );