let S1, S2 be non empty gate`1=arity ManySortedSign ; :: thesis: S1 +* S2 is gate`1=arity
set S = S1 +* S2;
A1: ( the carrier' of (S1 +* S2) = the carrier' of S1 \/ the carrier' of S2 & the Arity of (S1 +* S2) = the Arity of S1 +* the Arity of S2 ) by Def2;
let g be set ; :: according to CIRCCOMB:def 8 :: thesis: ( g in the carrier' of (S1 +* S2) implies g = [(the Arity of (S1 +* S2) . g),(g `2 )] )
assume A2: g in the carrier' of (S1 +* S2) ; :: thesis: g = [(the Arity of (S1 +* S2) . g),(g `2 )]
then reconsider g = g as Gate of (S1 +* S2) ;
A3: ( g in the carrier' of S1 or g in the carrier' of S2 ) by A1, A2, XBOOLE_0:def 3;
A4: ( dom the Arity of (S1 +* S2) = the carrier' of (S1 +* S2) & dom the Arity of S1 = the carrier' of S1 & dom the Arity of S2 = the carrier' of S2 ) by FUNCT_2:def 1;

A5: now

assume A6: not g in the carrier' of S2 ; :: thesis: g = [(the Arity of (S1 +* S2) . g),(g `2 )]
then reconsider g1 = g as Gate of S1 by A1, A2, XBOOLE_0:def 3;
thus g = [(the Arity of S1 . g1),(g `2 )] by A3, A6, Def8
.= [(the Arity of (S1 +* S2) . g),(g `2 )] by A1, A2, A4, A6, FUNCT_4:def 1 ; :: thesis: verum

end;

now

assume A7: g in the carrier' of S2 ; :: thesis: g = [(the Arity of (S1 +* S2) . g),(g `2 )]
then reconsider g2 = g as Gate of S2 ;
thus g = [(the Arity of S2 . g2),(g `2 )] by A7, Def8
.= [(the Arity of (S1 +* S2) . g),(g `2 )] by A1, A4, A7, FUNCT_4:def 1 ; :: thesis: verum

end;

hence g = [(the Arity of (S1 +* S2) . g),(g `2 )] by A5; :: thesis: verum