:: deftheorem Def6 defines Inv PRALG_1:def 6 :
for A, B being non empty set
for b₃ being Function of [:A,B:],[:B,A:] holds
( b₃ = Inv (A,B) iff for a being Element of [:A,B:] holds b₃ . a = [(a `2),(a `1)] );