thus ( p = r implies for a being FinSequence of D holds
( a in p iff a in r ) ) ; :: thesis: ( ( for a being FinSequence of D holds
( a in p iff a in r ) ) implies p = r )
thus ( ( for a being FinSequence of D holds
( a in p iff a in r ) ) implies p = r ) :: thesis: verum

proof

assume A1: for a being FinSequence of D holds
( a in p iff a in r ) ; :: thesis: p = r

now :: thesis: for x being set holds
( x in p iff x in r )

let x be set ; :: thesis: ( x in p iff x in r )

A2: now :: thesis: ( x in r implies x in p )

assume A3: x in r ; :: thesis: x in p
r is Subset of (D *) by Def7;
then x is FinSequence of D by A3, FINSEQ_1:def 11;
hence x in p by A1, A3; :: thesis: verum

end;

now :: thesis: ( x in p implies x in r )

assume A4: x in p ; :: thesis: x in r
p is Subset of (D *) by Def7;
then x is FinSequence of D by A4, FINSEQ_1:def 11;
hence x in r by A1, A4; :: thesis: verum

end;

hence ( x in p iff x in r ) by A2; :: thesis: verum

end;

hence p = r by TARSKI:1; :: thesis: verum

end;