let S1, S2 be non empty Circuit-like ManySortedSign ; :: thesis: ( InnerVertices S1 misses InnerVertices S2 implies S1 +* S2 is Circuit-like )
assume A1: InnerVertices S1 misses InnerVertices S2 ; :: thesis: S1 +* S2 is Circuit-like
let S be non empty non void ManySortedSign ; :: according to MSAFREE2:def 6 :: thesis: ( not S = S1 +* S2 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 = S1 +* S2 ; :: 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₂ )
set r = the ResultSort of S;
set r1 = the ResultSort of S1;
set r2 = the ResultSort of S2;
let o1, o2 be Gate of S; :: thesis: ( not the_result_sort_of o1 = the_result_sort_of o2 or o1 = o2 )
assume A3: the_result_sort_of o1 = the_result_sort_of o2 ; :: thesis: o1 = o2
A4: ( the ResultSort of S = the ResultSort of S1 +* the ResultSort of S2 & dom the ResultSort of S = the carrier' of S & dom the ResultSort of S1 = the carrier' of S1 & dom the ResultSort of S2 = the carrier' of S2 ) by A2, Def2, FUNCT_2:def 1;
A5: ( o1 in the carrier' of S & o2 in the carrier' of S & the carrier' of S = the carrier' of S1 \/ the carrier' of S2 ) by A2, Def2;
then ( ( ( not o1 in the carrier' of S2 & o1 in the carrier' of S1 ) or o1 in the carrier' of S2 ) & ( ( not o2 in the carrier' of S2 & o2 in the carrier' of S1 ) or o2 in the carrier' of S2 ) ) by XBOOLE_0:def 3;
then A6: ( ( ( the ResultSort of S . o1 = the ResultSort of S1 . o1 & the ResultSort of S1 . o1 in rng the ResultSort of S1 & o1 in the carrier' of S1 ) or ( the ResultSort of S . o1 = the ResultSort of S2 . o1 & the ResultSort of S2 . o1 in rng the ResultSort of S2 & o1 in the carrier' of S2 ) ) & ( ( the ResultSort of S . o2 = the ResultSort of S1 . o2 & the ResultSort of S1 . o2 in rng the ResultSort of S1 & o2 in the carrier' of S1 ) or ( the ResultSort of S . o2 = the ResultSort of S2 . o2 & the ResultSort of S2 . o2 in rng the ResultSort of S2 & o2 in the carrier' of S2 ) ) ) by A4, A5, FUNCT_1:def 5, FUNCT_4:def 1;

per cases ( ( the ResultSort of S . o1 = the ResultSort of S1 . o1 & o1 in the carrier' of S1 & the ResultSort of S . o2 = the ResultSort of S1 . o2 & o2 in the carrier' of S1 ) or ( the ResultSort of S . o1 = the ResultSort of S2 . o1 & o1 in the carrier' of S2 & the ResultSort of S . o2 = the ResultSort of S2 . o2 & o2 in the carrier' of S2 ) ) by A1, A3, A6, XBOOLE_0:3;

suppose A7: ( the ResultSort of S . o1 = the ResultSort of S1 . o1 & o1 in the carrier' of S1 & the ResultSort of S . o2 = the ResultSort of S1 . o2 & o2 in the carrier' of S1 ) ; :: thesis: o1 = o2

then reconsider S = S1 as non empty non void Circuit-like ManySortedSign ;
reconsider p1 = o1, p2 = o2 as Gate of S by A7;
( the_result_sort_of p1 = the ResultSort of S1 . p1 & the_result_sort_of p2 = the ResultSort of S1 . p2 ) ;
hence o1 = o2 by A3, A7, MSAFREE2:def 6; :: thesis: verum

end;

suppose A8: ( the ResultSort of S . o1 = the ResultSort of S2 . o1 & o1 in the carrier' of S2 & the ResultSort of S . o2 = the ResultSort of S2 . o2 & o2 in the carrier' of S2 ) ; :: thesis: o1 = o2

then reconsider S = S2 as non empty non void Circuit-like ManySortedSign ;
reconsider p1 = o1, p2 = o2 as Gate of S by A8;
( the_result_sort_of p1 = the ResultSort of S2 . p1 & the_result_sort_of p2 = the ResultSort of S2 . p2 ) ;
hence o1 = o2 by A3, A8, MSAFREE2:def 6; :: thesis: verum

end;

end;