let f be one-to-one Function; :: thesis: for S1, S2 being non empty Circuit-like ManySortedSign st the ResultSort of S1 c= f & the ResultSort of S2 c= f holds
S1 +* S2 is Circuit-like
let S1, S2 be non empty Circuit-like ManySortedSign ; :: thesis: ( the ResultSort of S1 c= f & the ResultSort of S2 c= f implies S1 +* S2 is Circuit-like )
assume A1: ( the ResultSort of S1 c= f & the ResultSort of S2 c= f ) ; :: 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₂ ) )
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;
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 ) by A2, Def2, FUNCT_2:def 1;
( the ResultSort of S1 +* the ResultSort of S2 c= the ResultSort of S1 \/ the ResultSort of S2 & the ResultSort of S1 \/ the ResultSort of S2 c= f ) by A1, FUNCT_4:30, XBOOLE_1:8;
then A5: ( the ResultSort of S1 +* the ResultSort of S2 c= f & o1 in dom the ResultSort of S & o2 in dom the ResultSort of S ) by A4, XBOOLE_1:1;
then ( the ResultSort of S . o1 = f . o1 & the ResultSort of S . o2 = f . o2 & dom the ResultSort of S c= dom f ) by A4, GRFUNC_1:8;
hence o1 = o2 by A3, A5, FUNCT_1:def 8; :: thesis: verum