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