:: deftheorem defines tohilb HILBERT4:def 5 :
for x being set holds x tohilb = ((id 1) +* ([:1,(Funcs (x,{})):] * [:(Funcs (x,{})),{1}:])) +* ([:{1},(Funcs (x,{})):] * [:(Funcs (x,{})),{0}:]);