take i |-> the Element of D ; :: thesis: ( i |-> the Element of D is Element of bool [:NAT ,D:] & i |-> the Element of D is FinSequence of D & i |-> the Element of D is i -long )
thus ( i |-> the Element of D is Element of bool [:NAT ,D:] & i |-> the Element of D is FinSequence of D & i |-> the Element of D is i -long ) by Th77; :: thesis: verum