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 that
A1: the ResultSort of S1 c= f and
A2: the ResultSort of S2 c= f ; :: 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₂ ) )
set r1 = the ResultSort of S1;
set r2 = the ResultSort of S2;
set r = the ResultSort of S;
A3: the ResultSort of S1 +* the ResultSort of S2 c= the ResultSort of S1 \/ the ResultSort of S2 by FUNCT_4:29;
assume 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;
the ResultSort of S1 \/ the ResultSort of S2 c= f by A1, A2, XBOOLE_1:8;
then A5: the ResultSort of S1 +* the ResultSort of S2 c= f by A3;
then A6: dom the ResultSort of S c= dom f by A4, GRFUNC_1:2;
let o1, o2 be Gate of S; :: thesis: ( not the_result_sort_of o1 = the_result_sort_of o2 or o1 = o2 )
A7: dom the ResultSort of S = the carrier' of S by FUNCT_2:def 1;
then A8: o1 in dom the ResultSort of S ;
A9: o2 in dom the ResultSort of S by A7;
assume A10: the_result_sort_of o1 = the_result_sort_of o2 ; :: thesis: o1 = o2
A11: the ResultSort of S . o2 = f . o2 by A4, A7, A5, GRFUNC_1:2;
the ResultSort of S . o1 = f . o1 by A4, A7, A5, GRFUNC_1:2;
hence o1 = o2 by A10, A8, A9, A11, A6, FUNCT_1:def 4; :: thesis: verum