let S1, S2, S3 be non empty ManySortedSign ; :: thesis: ( S1 tolerates S2 & S2 tolerates S3 & S3 tolerates S1 implies S1 +* S2 tolerates S3 )
assume that
A1: the Arity of S1 tolerates the Arity of S2 and
A2: the ResultSort of S1 tolerates the ResultSort of S2 and
A3: the Arity of S2 tolerates the Arity of S3 and
A4: the ResultSort of S2 tolerates the ResultSort of S3 and
A5: the Arity of S3 tolerates the Arity of S1 and
A6: the ResultSort of S3 tolerates the ResultSort of S1 ; :: according to CIRCCOMB:def 1 :: thesis: S1 +* S2 tolerates S3
the Arity of (S1 +* S2) = the Arity of S1 +* the Arity of S2 by Def2;
hence the Arity of (S1 +* S2) tolerates the Arity of S3 by A1, A3, A5, FUNCT_4:125; :: according to CIRCCOMB:def 1 :: thesis: the ResultSort of (S1 +* S2) tolerates the ResultSort of S3
the ResultSort of (S1 +* S2) = the ResultSort of S1 +* the ResultSort of S2 by Def2;
hence the ResultSort of (S1 +* S2) tolerates the ResultSort of S3 by A2, A4, A6, FUNCT_4:125; :: thesis: verum