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 S' be non empty non void ManySortedSign ; :: according to MSAFREE2:def 6 :: thesis: ( not S' = S or for b₁, b₂ being Element of the carrier' of S' holds
( not the_result_sort_of b₁ = the_result_sort_of b₂ or b₁ = b₂ ) )
assume A2: S' = S ; :: thesis: for b₁, b₂ being Element of the carrier' of S' holds
( not the_result_sort_of b₁ = the_result_sort_of b₂ or b₁ = b₂ )
let o1, o2 be Gate of S'; :: thesis: ( not the_result_sort_of o1 = the_result_sort_of o2 or o1 = o2 )
( the_result_sort_of o1 = the ResultSort of S . o1 & o1 in the carrier' of S & o2 in the carrier' of S & the_result_sort_of o2 = the ResultSort of S . o2 ) by A2;
then ( the_result_sort_of o1 = o1 & the_result_sort_of o2 = o2 ) by A1, FUNCT_1:34;
hence ( not the_result_sort_of o1 = the_result_sort_of o2 or o1 = o2 ) ; :: thesis: verum