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