let S1, S2 be non empty unsplit gate`1=arity ManySortedSign ; :: thesis: S1 tolerates S2
set A1 = the Arity of S1;
set A2 = the Arity of S2;
set R1 = the ResultSort of S1;
set R2 = the ResultSort of S2;
thus the Arity of S1 tolerates the Arity of S2 :: according to CIRCCOMB:def 1 :: thesis: the ResultSort of S1 tolerates the ResultSort of S2

proof

let x be set ; :: according to PARTFUN1:def 6 :: thesis: ( not x in (dom the Arity of S1) /\ (dom the Arity of S2) or the Arity of S1 . x = the Arity of S2 . x )
assume x in (dom the Arity of S1) /\ (dom the Arity of S2) ; :: thesis: the Arity of S1 . x = the Arity of S2 . x
then ( x in dom the Arity of S1 & x in dom the Arity of S2 ) by XBOOLE_0:def 4;
then ( x in the carrier' of S1 & x in the carrier' of S2 ) by FUNCT_2:def 1;
then ( x = [(the Arity of S1 . x),(x `2 )] & x = [(the Arity of S2 . x),(x `2 )] ) by Def8;
hence the Arity of S1 . x = the Arity of S2 . x by ZFMISC_1:33; :: thesis: verum

end;

let x be set ; :: according to PARTFUN1:def 6 :: thesis: ( not x in (dom the ResultSort of S1) /\ (dom the ResultSort of S2) or the ResultSort of S1 . x = the ResultSort of S2 . x )
assume x in (dom the ResultSort of S1) /\ (dom the ResultSort of S2) ; :: thesis: the ResultSort of S1 . x = the ResultSort of S2 . x
then ( x in dom the ResultSort of S1 & x in dom the ResultSort of S2 ) by XBOOLE_0:def 4;
then ( x in the carrier' of S1 & x in the carrier' of S2 ) by FUNCT_2:def 1;
then ( the ResultSort of S1 . x = x & the ResultSort of S2 . x = x ) by Th52;
hence the ResultSort of S1 . x = the ResultSort of S2 . x ; :: thesis: verum