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
A2: 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
A3: 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 object ; :: thesis: ( x in L1 implies x in L2 )
assume A4: x in L1 ; :: thesis: x in L2
then reconsider p = x as FinSequence of Vars by FINSEQ_2:def 3;
A5: p is one-to-one by A2, A4;
for i being Nat st i in dom p holds
(p . i) `1 c= rng (p | i) by A2, A4;
hence x in L2 by A3, A5; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in L2 or x in L1 )
assume A6: x in L2 ; :: thesis: x in L1
then reconsider p = x as FinSequence of Vars by FINSEQ_2:def 3;
A7: p is one-to-one by A3, A6;
for i being Nat st i in dom p holds
(p . i) `1 c= rng (p | i) by A3, A6;
hence x in L1 by A2, A7; :: thesis: verum