let F be Element of Funcs (A,BOOLEAN); :: thesis: F is boolean-valued
ex f being Function st
( F = f & dom f = A & rng f c= BOOLEAN ) by FUNCT_2:def 2;
hence rng F c= BOOLEAN ; :: according to MARGREL1:def 16 :: thesis: verum