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 -element )
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 -element ) by Th77; :: thesis: verum