theorem
for
S1,
S2 being
ManySortedSign st
ManySortedSign(# the
carrier of
S1, the
carrier' of
S1, the
Arity of
S1, the
ResultSort of
S1 #)
= ManySortedSign(# the
carrier of
S2, the
carrier' of
S2, the
Arity of
S2, the
ResultSort of
S2 #) holds
for
o,
a being
set for
r1 being
Element of
S1 for
r2 being
Element of
S2 st
r1 = r2 &
o is_of_type a,
r1 holds
o is_of_type a,
r2 ;