let it1, it2 be FinSequence-DOMAIN of ; :: thesis: ( ( for x being set holds
( x in it1 iff x is cyclic Path of cyclic ) ) & ( for x being set holds
( x in it2 iff x is cyclic Path of cyclic ) ) implies it1 = it2 )
assume that
A2: for x being set holds
( x in it1 iff x is cyclic Path of cyclic ) and
A3: for x being set holds
( x in it2 iff x is cyclic Path of cyclic ) ; :: thesis: it1 = it2

now

let x be set ; :: thesis: ( x in it1 iff x in it2 )
( x in it1 iff x is cyclic Path of cyclic ) by A2;
hence ( x in it1 iff x in it2 ) by A3; :: thesis: verum

end;

hence it1 = it2 by TARSKI:2; :: thesis: verum