let S1, S2 be non empty gate`1=arity ManySortedSign ; :: thesis: S1 +* S2 is gate`1=arity
set S = S1 +* S2;
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)] )
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) ; :: thesis: 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 :: thesis: ( 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 ; :: thesis: 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 ; :: thesis: verum
end;
now :: thesis: ( g in the carrier' of S2 implies g = [( the Arity of (S1 +* S2) . g),(g `2)] )
assume A9: 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 A9, Def8
.= [( the Arity of (S1 +* S2) . g),(g `2)] by A5, A2, A1, A4, A9, FUNCT_4:def 1 ; :: thesis: verum
end;
hence g = [( the Arity of (S1 +* S2) . g),(g `2)] by A7; :: thesis: verum