theorem Th4: :: BVFUNC_1:5

for Y being non empty set
for a being Function of Y,BOOLEAN holds a '&' (O_el Y) = O_el Y