:: deftheorem defines [[: PRALG_2:def 3 :
for I being non empty set
for A, B being non-empty ManySortedSet of I
for pj being Element of I *
for rj being Element of I
for f being Function of ((A #) . pj),(A . rj)
for g being Function of ((B #) . pj),(B . rj)
for b₈ being Function of (([|A,B|] #) . pj),([|A,B|] . rj) holds
( b₈ = [[:f,g:]] iff for h being Function st h in ([|A,B|] #) . pj holds
b₈ . h = [(f . (pr1 h)),(g . (pr2 h))] );