let S1, S2 be ManySortedSet of the carrier of (X -CircuitStr); :: 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 :: thesis: for x being object st x in the carrier of (X -CircuitStr) holds
S1 . x = S2 . x

let x be object ; :: 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 ; :: thesis: verum