theorem :: HILBERT3:32

for p, q being Element of HP-WFF
for V being SetValuation holds SetVal (V,(p => q)) = Funcs ((SetVal (V,p)),(SetVal (V,q))) by Def2;