thus F . p is Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) ; :: thesis: verum