:: deftheorem defines is_a_system_of_different_representatives_of HALLMAR1:def 3 :
for F being finite set
for X being FinSequence of bool F
for A being set holds
( A is_a_system_of_different_representatives_of X iff ex f being FinSequence of F st
( f = A & dom X = dom f & ( for i being Element of NAT st i in dom f holds
f . i in X . i ) & f is one-to-one ) );