let S1, S2 be non empty gate`1=arity ManySortedSign ; S1 +* S2 is gate`1=arity
set S = S1 +* S2;
let g be set ; CIRCCOMB:def 8 ( g in the carrier' of (S1 +* S2) implies g = [( the Arity of (S1 +* S2) . g),(g `2)] )
A1:
dom the Arity of S1 = the carrier' of S1
by FUNCT_2:def 1;
A2:
the Arity of (S1 +* S2) = the Arity of S1 +* the Arity of S2
by Def2;
assume A3:
g in the carrier' of (S1 +* S2)
; g = [( the Arity of (S1 +* S2) . g),(g `2)]
then reconsider g = g as Gate of (S1 +* S2) ;
A4:
dom the Arity of S2 = the carrier' of S2
by FUNCT_2:def 1;
A5:
the carrier' of (S1 +* S2) = the carrier' of S1 \/ the carrier' of S2
by Def2;
then A6:
( g in the carrier' of S1 or g in the carrier' of S2 )
by A3, XBOOLE_0:def 3;
A7:
now ( not g in the carrier' of S2 implies g = [( the Arity of (S1 +* S2) . g),(g `2)] )assume A8:
not
g in the
carrier' of
S2
;
g = [( the Arity of (S1 +* S2) . g),(g `2)]then reconsider g1 =
g as
Gate of
S1 by A5, A3, XBOOLE_0:def 3;
thus g =
[( the Arity of S1 . g1),(g `2)]
by A6, A8, Def8
.=
[( the Arity of (S1 +* S2) . g),(g `2)]
by A5, A2, A3, A1, A4, A8, FUNCT_4:def 1
;
verum end;
hence
g = [( the Arity of (S1 +* S2) . g),(g `2)]
by A7; verum