let T be set ; :: thesis: for S being SetSequence of T st S is constant holds
the_value_of S is Subset of T
let S be SetSequence of T; :: thesis: ( S is constant implies the_value_of S is Subset of T )
assume S is constant ; :: thesis: the_value_of S is Subset of T
then consider x being set such that
A1: x in dom S and
A2: the_value_of S = S . x by FUNCT_1:def 12;
reconsider n = x as Element of NAT by A1;
S . n in bool T ;
hence the_value_of S is Subset of T by A2; :: thesis: verum