:: deftheorem defines MSS_morph MSALIMIT:def 10 :
for S1, S2 being ManySortedSign
for b₃ being set holds
( b₃ = MSS_morph (S1,S2) iff for x being set holds
( x in b₃ iff ex f, g being Function st
( x = [f,g] & f,g form_morphism_between S1,S2 ) ) );