consider g being Function of S,T, d being Function of T,S;
take [g,d] ; :: thesis: ex g being Function of S,T ex d being Function of T,S st [g,d] = [g,d]
thus ex g being Function of S,T ex d being Function of T,S st [g,d] = [g,d] ; :: thesis: verum