let S1, S2, S3 be non empty ManySortedSign ; for A1 being non-empty MSAlgebra over S1
for A2 being non-empty MSAlgebra over S2
for A3 being MSAlgebra over S3 st A1 tolerates A2 & A2 tolerates A3 & A3 tolerates A1 holds
A1 +* A2 tolerates A3
let A1 be non-empty MSAlgebra over S1; for A2 being non-empty MSAlgebra over S2
for A3 being MSAlgebra over S3 st A1 tolerates A2 & A2 tolerates A3 & A3 tolerates A1 holds
A1 +* A2 tolerates A3
let A2 be non-empty MSAlgebra over S2; for A3 being MSAlgebra over S3 st A1 tolerates A2 & A2 tolerates A3 & A3 tolerates A1 holds
A1 +* A2 tolerates A3
let A3 be MSAlgebra over S3; ( A1 tolerates A2 & A2 tolerates A3 & A3 tolerates A1 implies A1 +* A2 tolerates A3 )
assume that
A1:
S1 tolerates S2
and
A2:
the Sorts of A1 tolerates the Sorts of A2
and
A3:
the Charact of A1 tolerates the Charact of A2
and
A4:
S2 tolerates S3
and
A5:
the Sorts of A2 tolerates the Sorts of A3
and
A6:
the Charact of A2 tolerates the Charact of A3
and
A7:
S3 tolerates S1
and
A8:
the Sorts of A3 tolerates the Sorts of A1
and
A9:
the Charact of A3 tolerates the Charact of A1
; CIRCCOMB:def 3 A1 +* A2 tolerates A3
thus
S1 +* S2 tolerates S3
by A1, A4, A7, Th3; CIRCCOMB:def 3 ( the Sorts of (A1 +* A2) tolerates the Sorts of A3 & the Charact of (A1 +* A2) tolerates the Charact of A3 )
the Sorts of (A1 +* A2) = the Sorts of A1 +* the Sorts of A2
by A2, Def4;
hence
the Sorts of (A1 +* A2) tolerates the Sorts of A3
by A2, A5, A8, FUNCT_4:125; the Charact of (A1 +* A2) tolerates the Charact of A3
the Charact of (A1 +* A2) = the Charact of A1 +* the Charact of A2
by A2, Def4;
hence
the Charact of (A1 +* A2) tolerates the Charact of A3
by A3, A6, A9, FUNCT_4:125; verum