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
set r1 = the ResultSort of S1;
set r2 = the ResultSort of S2;
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₂ ) )
set r = the ResultSort of S;
A2: dom the ResultSort of S1 = the carrier' of S1 by FUNCT_2:def 1;
assume A3: 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₂ )
then A4: the ResultSort of S = the ResultSort of S1 +* the ResultSort of S2 by Def2;
A5: dom the ResultSort of S2 = the carrier' of S2 by FUNCT_2:def 1;
let o1, o2 be Gate of S; :: thesis: ( not the_result_sort_of o1 = the_result_sort_of o2 or o1 = o2 )
A6: the carrier' of S = the carrier' of S1 \/ the carrier' of S2 by A3, Def2;
then ( ( not o1 in the carrier' of S2 & o1 in the carrier' of S1 ) or o1 in the carrier' of S2 ) by XBOOLE_0:def 3;
then A7: ( ( 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 ) ) by A4, A2, A5, A6, FUNCT_1:def 3, FUNCT_4:def 1;
( ( not o2 in the carrier' of S2 & o2 in the carrier' of S1 ) or o2 in the carrier' of S2 ) by A6, XBOOLE_0:def 3;
then A8: ( ( 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, A2, A5, A6, FUNCT_1:def 3, FUNCT_4:def 1;
assume A9: the_result_sort_of o1 = the_result_sort_of o2 ; :: thesis: o1 = o2

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, A9, A7, A8, XBOOLE_0:3;

suppose A10: ( 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 A10;
A11: the_result_sort_of p2 = the ResultSort of S1 . p2 ;
the_result_sort_of p1 = the ResultSort of S1 . p1 ;
hence o1 = o2 by A9, A10, A11, MSAFREE2:def 6; :: thesis: verum

end;

suppose A12: ( 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 A12;
A13: the_result_sort_of p2 = the ResultSort of S2 . p2 ;
the_result_sort_of p1 = the ResultSort of S2 . p1 ;
hence o1 = o2 by A9, A12, A13, MSAFREE2:def 6; :: thesis: verum

end;

end;