let A1, A2 be set ; :: thesis: ( ( for X being set holds
( X in A1 iff ( X c= D * & ( for a, b being FinSequence of D st a in X & b in X holds
len a = len b ) ) ) ) & ( for X being set holds
( X in A2 iff ( X c= D * & ( for a, b being FinSequence of D st a in X & b in X holds
len a = len b ) ) ) ) implies A1 = A2 )
assume that
A2: for X being set holds
( X in A1 iff ( X c= D * & ( for a, b being FinSequence of D st a in X & b in X holds
len a = len b ) ) ) and
A3: for X being set holds
( X in A2 iff ( X c= D * & ( for a, b being FinSequence of D st a in X & b in X holds
len a = len b ) ) ) ; :: thesis: A1 = A2
for x being object holds
( x in A1 iff x in A2 )

proof

let x be object ; :: thesis: ( x in A1 iff x in A2 )
reconsider xx = x as set by TARSKI:1;
thus ( x in A1 implies x in A2 ) :: thesis: ( x in A2 implies x in A1 )

proof

assume A4: x in A1 ; :: thesis: x in A2
then A5: for a, b being FinSequence of D st a in xx & b in xx holds
len a = len b by A2;
xx c= D * by A2, A4;
hence x in A2 by A3, A5; :: thesis: verum

end;

thus ( x in A2 implies x in A1 ) :: thesis: verum

proof

assume A6: x in A2 ; :: thesis: x in A1
then A7: for a, b being FinSequence of D st a in xx & b in xx holds
len a = len b by A3;
xx c= D * by A3, A6;
hence x in A1 by A2, A7; :: thesis: verum

end;

end;

hence A1 = A2 by TARSKI:2; :: thesis: verum