let f be FinSequence of Si; :: thesis: f is FinSequence of bool X
thus rng f c= bool X by XBOOLE_1:1; :: according to FINSEQ_1:def 4 :: thesis: verum