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 object ; :: according to PARTFUN1:def 4 :: thesis: ( not x in (proj1 the Arity of S1) /\ (proj1 the Arity of S2) or the Arity of S1 . x = the Arity of S2 . x )
assume A1: 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 S2 by XBOOLE_0:def 4;
then x in the carrier' of S2 by FUNCT_2:def 1;
then A2: x = [( the Arity of S2 . x),(x `2)] by Def8;
x in dom the Arity of S1 by A1, XBOOLE_0:def 4;
then x in the carrier' of S1 by FUNCT_2:def 1;
then x = [( the Arity of S1 . x),(x `2)] by Def8;
hence the Arity of S1 . x = the Arity of S2 . x by A2, XTUPLE_0:1; :: thesis: verum
end;
let x be object ; :: according to PARTFUN1:def 4 :: thesis: ( not x in (proj1 the ResultSort of S1) /\ (proj1 the ResultSort of S2) or the ResultSort of S1 . x = the ResultSort of S2 . x )
assume A3: 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 by XBOOLE_0:def 4;
then x in the carrier' of S1 by FUNCT_2:def 1;
then A4: the ResultSort of S1 . x = x by Th44;
x in dom the ResultSort of S2 by A3, XBOOLE_0:def 4;
then x in the carrier' of S2 by FUNCT_2:def 1;
hence the ResultSort of S1 . x = the ResultSort of S2 . x by A4, Th44; :: thesis: verum