let S be non empty ManySortedSign ; :: thesis: ( S is void implies S is Circuit-like )
assume A1: S is void ; :: thesis: S is Circuit-like
let S9 be non empty non void ManySortedSign ; :: according to MSAFREE2:def 6 :: thesis: ( S9 = S implies for o1, o2 being OperSymbol of S9 st the_result_sort_of o1 = the_result_sort_of o2 holds
o1 = o2 )
thus ( S9 = S implies for o1, o2 being OperSymbol of S9 st the_result_sort_of o1 = the_result_sort_of o2 holds
o1 = o2 ) by A1; :: thesis: verum