let L1, L2 be FinSequenceSet of Vars ; :: thesis: ( ( for p being FinSequence of Vars holds
( p in L1 iff ( p is one-to-one & ( for i being Nat st i in dom p holds
(p . i) `1 c= rng (p dom i) ) ) ) ) & ( for p being FinSequence of Vars holds
( p in L2 iff ( p is one-to-one & ( for i being Nat st i in dom p holds
(p . i) `1 c= rng (p dom i) ) ) ) ) implies L1 = L2 )
assume that
A1: for p being FinSequence of Vars holds
( p in L1 iff ( p is one-to-one & ( for i being Nat st i in dom p holds
(p . i) `1 c= rng (p | i) ) ) ) and
A2: for p being FinSequence of Vars holds
( p in L2 iff ( p is one-to-one & ( for i being Nat st i in dom p holds
(p . i) `1 c= rng (p | i) ) ) ) ; :: thesis: L1 = L2

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: L2 c= L1

let x be set ; :: thesis: ( x in L1 implies x in L2 )
assume A3: x in L1 ; :: thesis: x in L2
then reconsider p = x as FinSequence of Vars by FINSEQ_2:def 3;
( p is one-to-one & ( for i being Nat st i in dom p holds
(p . i) `1 c= rng (p | i) ) ) by A1, A3;
hence x in L2 by A2; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in L2 or x in L1 )
assume A4: x in L2 ; :: thesis: x in L1
then reconsider p = x as FinSequence of Vars by FINSEQ_2:def 3;
( p is one-to-one & ( for i being Nat st i in dom p holds
(p . i) `1 c= rng (p | i) ) ) by A2, A4;
hence x in L1 by A1; :: thesis: verum