let A, B be GeneratorSet of FreeMSA X; :: thesis: ( ( for s being SortSymbol of S holds A . s = FreeGen (s,X) ) & ( for s being SortSymbol of S holds B . s = FreeGen (s,X) ) implies A = B )
assume that
A59: for s being SortSymbol of S holds A . s = FreeGen (s,X) and
A60: for s being SortSymbol of S holds B . s = FreeGen (s,X) ; :: thesis: A = B
for i being object st i in the carrier of S holds
A . i = B . i

proof

let i be object ; :: thesis: ( i in the carrier of S implies A . i = B . i )
assume i in the carrier of S ; :: thesis: A . i = B . i
then reconsider s = i as SortSymbol of S ;
A . s = FreeGen (s,X) by A59;
hence A . i = B . i by A60; :: thesis: verum

end;

hence A = B ; :: thesis: verum