defpred S1[ object ] means ex p being Function st
( p = $1 & p is one-to-one & ( for i being Nat st i in dom p holds
(p . i) `1 c= rng (p | i) ) );
consider L being set such that
A1: for x being object holds
( x in L iff ( x in Vars * & S1[x] ) ) from XBOOLE_0:sch 1();
 L is FinSequenceSet of Vars
proof
let x be object ; :: according to FINSEQ_2:def 3 :: thesis: ( not x in L or x is FinSequence of Vars )
assume x in L ; :: thesis: x is FinSequence of Vars
then x in Vars * by A1;
hence x is FinSequence of Vars by FINSEQ_1:def 11; :: thesis: verum
end;
then reconsider L = L as FinSequenceSet of Vars ;
take L ; :: thesis: for p being FinSequence of Vars holds
( p in L iff ( p is one-to-one & ( for i being Nat st i in dom p holds
(p . i) `1 c= rng (p dom i) ) ) )
let p be FinSequence of Vars ; :: thesis: ( p in L iff ( p is one-to-one & ( for i being Nat st i in dom p holds
(p . i) `1 c= rng (p dom i) ) ) )
( p in L iff ( p in Vars * & ex q being Function st
( q = p & q is one-to-one & ( for i being Nat st i in dom q holds
(q . i) `1 c= rng (q | i) ) ) ) ) by A1;
hence ( p in L iff ( p is one-to-one & ( for i being Nat st i in dom p holds
(p . i) `1 c= rng (p dom i) ) ) ) by FINSEQ_1:def 11; :: thesis: verum