let S1, S2 be non empty ManySortedSign ; :: thesis: ( S1 is gate`2isBoolean & S2 is gate`2isBoolean implies S1 +* S2 is gate`2isBoolean )
set S = S1 +* S2;
assume that
A1: S1 is gate`2isBoolean and
A2: S2 is gate`2isBoolean ; :: thesis: S1 +* S2 is gate`2isBoolean
let g be set ; :: according to CIRCCOMB:def 9 :: thesis: ( g in the carrier' of (S1 +* S2) implies for p being FinSequence st p = the Arity of (S1 +* S2) . g holds
ex f being Function of ((len p) -tuples_on BOOLEAN),BOOLEAN st g = [(g `1),f] )
assume A3: g in the carrier' of (S1 +* S2) ; :: thesis: for p being FinSequence st p = the Arity of (S1 +* S2) . g holds
ex f being Function of ((len p) -tuples_on BOOLEAN),BOOLEAN st g = [(g `1),f]
let p be FinSequence; :: thesis: ( p = the Arity of (S1 +* S2) . g implies ex f being Function of ((len p) -tuples_on BOOLEAN),BOOLEAN st g = [(g `1),f] )
assume A4: p = the Arity of (S1 +* S2) . g ; :: thesis: ex f being Function of ((len p) -tuples_on BOOLEAN),BOOLEAN st g = [(g `1),f]
reconsider g = g as Gate of (S1 +* S2) by A3;
A5: dom the Arity of S1 = the carrier' of S1 by FUNCT_2:def 1;
A6: the Arity of (S1 +* S2) = the Arity of S1 +* the Arity of S2 by Def2;
A7: dom the Arity of S2 = the carrier' of S2 by FUNCT_2:def 1;
A8: the carrier' of (S1 +* S2) = the carrier' of S1 \/ the carrier' of S2 by Def2;
then A9: ( g in the carrier' of S1 or g in the carrier' of S2 ) by A3, XBOOLE_0:def 3;

A10: now :: thesis: ( not g in the carrier' of S2 implies ex f being Function of ((len p) -tuples_on BOOLEAN),BOOLEAN st g = [(g `1),f] )

assume A11: not g in the carrier' of S2 ; :: thesis: ex f being Function of ((len p) -tuples_on BOOLEAN),BOOLEAN st g = [(g `1),f]
then reconsider g1 = g as Gate of S1 by A8, A3, XBOOLE_0:def 3;
the Arity of S1 . g1 = p by A8, A6, A3, A4, A5, A7, A11, FUNCT_4:def 1;
hence ex f being Function of ((len p) -tuples_on BOOLEAN),BOOLEAN st g = [(g `1),f] by A1, A9, A11; :: thesis: verum

end;

now :: thesis: ( g in the carrier' of S2 implies ex f being Function of ((len p) -tuples_on BOOLEAN),BOOLEAN st g = [(g `1),f] )

assume A12: g in the carrier' of S2 ; :: thesis: ex f being Function of ((len p) -tuples_on BOOLEAN),BOOLEAN st g = [(g `1),f]
then reconsider g2 = g as Gate of S2 ;
the Arity of S2 . g2 = p by A8, A6, A4, A5, A7, A12, FUNCT_4:def 1;
hence ex f being Function of ((len p) -tuples_on BOOLEAN),BOOLEAN st g = [(g `1),f] by A2, A12; :: thesis: verum

end;

hence ex f being Function of ((len p) -tuples_on BOOLEAN),BOOLEAN st g = [(g `1),f] by A10; :: thesis: verum