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 b1, b2 being Element of the carrier' of S holds
( not the_result_sort_of b1 = the_result_sort_of b2 or b1 = b2 ) )
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 b1, b2 being Element of the carrier' of S holds
( not the_result_sort_of b1 = the_result_sort_of b2 or b1 = b2 )
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;