let X, Y be set ; :: thesis: ( ( for a being object holds
( a in X iff a is FinSequence of CQC-WFF Al ) ) & ( for a being object holds
( a in Y iff a is FinSequence of CQC-WFF Al ) ) implies X = Y )
assume that
A2: for a being object holds
( a in X iff a is FinSequence of CQC-WFF Al ) and
A3: for a being object holds
( a in Y iff a is FinSequence of CQC-WFF Al ) ; :: thesis: X = Y

now :: thesis: for a being object holds
( a in X iff a in Y )

let a be object ; :: thesis: ( a in X iff a in Y )
( a in X iff a is FinSequence of CQC-WFF Al ) by A2;
hence ( a in X iff a in Y ) by A3; :: thesis: verum

end;

hence X = Y by TARSKI:2; :: thesis: verum