take i |-> the Element of D ; :: thesis: ( i |-> the Element of D is Element of bool [:omega,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 [:omega,D:] & i |-> the Element of D is FinSequence of D & i |-> the Element of D is i -element ) by Th61; :: thesis: verum