let S be non empty ManySortedSign ; :: thesis: ( S is unsplit implies S is Circuit-like )
assume A1: the ResultSort of S = id the carrier' of S ; :: according to CIRCCOMB:def 7 :: thesis: S is Circuit-like
let S9 be non empty non void ManySortedSign ; :: according to MSAFREE2:def 6 :: thesis: ( not S9 = S or for b₁, b₂ being Element of the carrier' of S9 holds
( not the_result_sort_of b₁ = the_result_sort_of b₂ or b₁ = b₂ ) )
assume A2: S9 = S ; :: thesis: for b₁, b₂ being Element of the carrier' of S9 holds
( not the_result_sort_of b₁ = the_result_sort_of b₂ or b₁ = b₂ )
let o1, o2 be Gate of S9; :: thesis: ( not the_result_sort_of o1 = the_result_sort_of o2 or o1 = o2 )
thus ( not the_result_sort_of o1 = the_result_sort_of o2 or o1 = o2 ) by A1, A2, FUNCT_1:17; :: thesis: verum