let X be non empty finite set ; 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; 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; for A2 being Circuit of X,S2 holds A1 tolerates A2
let A2 be Circuit of X,S2; A1 tolerates A2
thus
S1 tolerates S2
by CIRCCOMB:47; CIRCCOMB:def 3 ( 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:80;
( 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:80;
hence
the Sorts of A1 tolerates the Sorts of A2
by A1, FUNCOP_1:87; the Charact of A1 tolerates the Charact of A2
thus
the Charact of A1 tolerates the Charact of A2
by CIRCCOMB:48; verum