let f be FinSequence of BOOLEAN ; :: thesis: f is boolean-valued
thus rng f c= BOOLEAN ; :: according to MARGREL1:def 16 :: thesis: verum