set g = the Function of S,T;
set d = the Function of T,S;
take
[ the Function of S,T, the Function of T,S]
; ( [ the Function of S,T, the Function of T,S] is set & ex g being Function of S,T ex d being Function of T,S st [ the Function of S,T, the Function of T,S] = [g,d] )
thus
( [ the Function of S,T, the Function of T,S] is set & ex g being Function of S,T ex d being Function of T,S st [ the Function of S,T, the Function of T,S] = [g,d] )
; verum