take {} ; :: thesis: for x being set st x in {} holds
x is Function of G,H
thus for x being set st x in {} holds
x is Function of G,H ; :: thesis: verum