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 17 :: thesis: verum