defpred S₁[ object ] means ex p being FinSequence st
( p = $1 & len p = len F & ( for i being Nat st i in dom p holds
p . i in dom (F . i) ) );
let IT1, IT2 be finite Subset of (NAT *); :: thesis: ( ( for x being object holds
( x in IT1 iff ex p being FinSequence st
( p = x & len p = len F & ( for i being Nat st i in dom p holds
p . i in dom (F . i) ) ) ) ) & ( for x being object holds
( x in IT2 iff ex p being FinSequence st
( p = x & len p = len F & ( for i being Nat st i in dom p holds
p . i in dom (F . i) ) ) ) ) implies IT1 = IT2 )
assume that
A35: for x being object holds
( x in IT1 iff S₁[x] ) and
A36: for x being object holds
( x in IT2 iff S₁[x] ) ; :: thesis: IT1 = IT2

now :: thesis: for x being object holds
( x in IT1 iff x in IT2 )

let x be object ; :: thesis: ( x in IT1 iff x in IT2 )
( x in IT1 iff S₁[x] ) by A35;
hence ( x in IT1 iff x in IT2 ) by A36; :: thesis: verum

end;

hence IT1 = IT2 by TARSKI:2; :: thesis: verum