let S1, S2 be ManySortedSet of ; :: thesis: ( ( for v being Vertex of (X -CircuitStr ) holds S1 . v = the_sort_of v,A ) & ( for v being Vertex of (X -CircuitStr ) holds S2 . v = the_sort_of v,A ) implies S1 = S2 )
assume that
A1: for v being Vertex of (X -CircuitStr ) holds S1 . v = the_sort_of v,A and
A2: for v being Vertex of (X -CircuitStr ) holds S2 . v = the_sort_of v,A ; :: thesis: S1 = S2

now

let x be set ; :: thesis: ( x in the carrier of (X -CircuitStr ) implies S1 . x = S2 . x )
assume x in the carrier of (X -CircuitStr ) ; :: thesis: S1 . x = S2 . x
then reconsider v = x as Vertex of (X -CircuitStr ) ;
thus S1 . x = the_sort_of v,A by A1
.= S2 . x by A2 ; :: thesis: verum

end;

hence S1 = S2 by PBOOLE:3; :: thesis: verum