defpred S_{1}[ object ] means $1 is one-to-one FinSequence of D;

consider X being set such that

A1: for x being object holds

( x in X iff ( x in bool [:NAT,D:] & S_{1}[x] ) )
from XBOOLE_0:sch 1();

take X ; :: thesis: for x being set holds

( x in X iff x is one-to-one FinSequence of D )

let x be set ; :: thesis: ( x in X iff x is one-to-one FinSequence of D )

thus ( x in X implies x is one-to-one FinSequence of D ) by A1; :: thesis: ( x is one-to-one FinSequence of D implies x in X )

assume x is one-to-one FinSequence of D ; :: thesis: x in X

then reconsider p = x as one-to-one FinSequence of D ;

p c= [:NAT,D:] ;

hence x in X by A1; :: thesis: verum

consider X being set such that

A1: for x being object holds

( x in X iff ( x in bool [:NAT,D:] & S

take X ; :: thesis: for x being set holds

( x in X iff x is one-to-one FinSequence of D )

let x be set ; :: thesis: ( x in X iff x is one-to-one FinSequence of D )

thus ( x in X implies x is one-to-one FinSequence of D ) by A1; :: thesis: ( x is one-to-one FinSequence of D implies x in X )

assume x is one-to-one FinSequence of D ; :: thesis: x in X

then reconsider p = x as one-to-one FinSequence of D ;

p c= [:NAT,D:] ;

hence x in X by A1; :: thesis: verum