deffunc H₁( Element of [:A,B:]) -> Element of [:B,A:] = [($1 `2),($1 `1)];
thus ex I being Function of [:A,B:],[:B,A:] st
for a being Element of [:A,B:] holds I . a = H₁(a) from FUNCT_2:sch 4(); :: thesis: verum