:: deftheorem defines [[: PRALG_2:def 4 :
for I being non empty set
for J being set
for A, B being V2() ManySortedSet of I
for p being Function of J,(I *)
for r being Function of J,I
for F being ManySortedFunction of (A #) * p,A * r
for G being ManySortedFunction of (B #) * p,B * r
for b₉ being ManySortedFunction of ([|A,B|] #) * p,[|A,B|] * r holds
( b₉ = [[:F,G:]] iff for j being object st j in J holds
for pj being Element of I *
for rj being Element of I st pj = p . j & rj = r . j holds
for f being Function of ((A #) . pj),(A . rj)
for g being Function of ((B #) . pj),(B . rj) st f = F . j & g = G . j holds
b₉ . j = [[:f,g:]] );