let S be non empty non void ManySortedSign ; :: thesis: for V being non-empty ManySortedSet of the carrier of S
for X1, X2 being SetWithCompoundTerm of S,V
for A being non-empty MSAlgebra over S holds X1 -Circuit A tolerates X2 -Circuit A
let V be non-empty ManySortedSet of the carrier of S; :: thesis: for X1, X2 being SetWithCompoundTerm of S,V
for A being non-empty MSAlgebra over S holds X1 -Circuit A tolerates X2 -Circuit A
let X1, X2 be SetWithCompoundTerm of S,V; :: thesis: for A being non-empty MSAlgebra over S holds X1 -Circuit A tolerates X2 -Circuit A
let A be non-empty MSAlgebra over S; :: thesis: X1 -Circuit A tolerates X2 -Circuit A
thus ( the Arity of (X1 -CircuitStr) tolerates the Arity of (X2 -CircuitStr) & the ResultSort of (X1 -CircuitStr) tolerates the ResultSort of (X2 -CircuitStr) ) by Th6; :: according to CIRCCOMB:def 1,CIRCCOMB:def 3 :: thesis: ( the Sorts of (X1 -Circuit A) tolerates the Sorts of (X2 -Circuit A) & the Charact of (X1 -Circuit A) tolerates the Charact of (X2 -Circuit A) )
thus the Sorts of (X1 -Circuit A) tolerates the Sorts of (X2 -Circuit A) :: thesis: the Charact of (X1 -Circuit A) tolerates the Charact of (X2 -Circuit A)

proof

let x be object ; :: according to PARTFUN1:def 4 :: thesis: ( not x in (proj1 the Sorts of (X1 -Circuit A)) /\ (proj1 the Sorts of (X2 -Circuit A)) or the Sorts of (X1 -Circuit A) . x = the Sorts of (X2 -Circuit A) . x )
assume A1: x in (dom the Sorts of (X1 -Circuit A)) /\ (dom the Sorts of (X2 -Circuit A)) ; :: thesis: the Sorts of (X1 -Circuit A) . x = the Sorts of (X2 -Circuit A) . x
then A2: x in dom the Sorts of (X1 -Circuit A) by XBOOLE_0:def 4;
A3: x in dom the Sorts of (X2 -Circuit A) by A1, XBOOLE_0:def 4;
A4: x in the carrier of (X1 -CircuitStr) by A2, PARTFUN1:def 2;
reconsider v1 = x as Vertex of (X1 -CircuitStr) by A2, PARTFUN1:def 2;
reconsider v2 = x as Vertex of (X2 -CircuitStr) by A3, PARTFUN1:def 2;
reconsider t = x as Term of S,V by A4, Th4;
thus the Sorts of (X1 -Circuit A) . x = the_sort_of (v1,A) by Def4
.= the Sorts of A . (the_sort_of t) by Def2
.= the_sort_of (v2,A) by Def2
.= the Sorts of (X2 -Circuit A) . x by Def4 ; :: thesis: verum

end;

let x be object ; :: according to PARTFUN1:def 4 :: thesis: ( not x in (proj1 the Charact of (X1 -Circuit A)) /\ (proj1 the Charact of (X2 -Circuit A)) or the Charact of (X1 -Circuit A) . x = the Charact of (X2 -Circuit A) . x )
assume A5: x in (dom the Charact of (X1 -Circuit A)) /\ (dom the Charact of (X2 -Circuit A)) ; :: thesis: the Charact of (X1 -Circuit A) . x = the Charact of (X2 -Circuit A) . x
then A6: x in dom the Charact of (X1 -Circuit A) by XBOOLE_0:def 4;
A7: x in dom the Charact of (X2 -Circuit A) by A5, XBOOLE_0:def 4;
reconsider g1 = x as Gate of (X1 -CircuitStr) by A6, PARTFUN1:def 2;
reconsider g2 = x as Gate of (X2 -CircuitStr) by A7, PARTFUN1:def 2;
thus the Charact of (X1 -Circuit A) . x = the_action_of (g1,A) by Def5
.= the Charact of A . ((g1 . {}) `1) by Def3
.= the_action_of (g2,A) by Def3
.= the Charact of (X2 -Circuit A) . x by Def5 ; :: thesis: verum