let X be non empty finite set ; :: thesis: for S1, S2 being Signature of X
for A1 being Circuit of X,S1
for A2 being Circuit of X,S2 holds A1 tolerates A2
let S1, S2 be Signature of X; :: thesis: for A1 being Circuit of X,S1
for A2 being Circuit of X,S2 holds A1 tolerates A2
let A1 be Circuit of X,S1; :: thesis: for A2 being Circuit of X,S2 holds A1 tolerates A2
let A2 be Circuit of X,S2; :: thesis: A1 tolerates A2
thus S1 tolerates S2 by CIRCCOMB:55; :: according to CIRCCOMB:def 3 :: thesis: ( the Sorts of A1 tolerates the Sorts of A2 & the Charact of A1 tolerates the Charact of A2 )
( the Sorts of A2 is constant & the_value_of the Sorts of A2 = X ) by Def10;
then A1: the Sorts of A2 = (dom the Sorts of A2) --> X by FUNCOP_1:95;
( the Sorts of A1 is constant & the_value_of the Sorts of A1 = X ) by Def10;
then the Sorts of A1 = (dom the Sorts of A1) --> X by FUNCOP_1:95;
hence the Sorts of A1 tolerates the Sorts of A2 by A1, CIRCCOMB:4; :: thesis: the Charact of A1 tolerates the Charact of A2
thus the Charact of A1 tolerates the Charact of A2 by CIRCCOMB:56; :: thesis: verum